mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
max_add_add_right : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : Add α] [AddRightMono α] (a b c : α), max (a + c) (b + c) = max a b + c
-- Mathlib.Geometry.Euclidean.MongePoint
/-- The position of the Monge point in relation to the circumcenter
and centroid.  -/
Affine.Simplex.mongePoint_eq_smul_vsub_vadd_circumcenter : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n),
  s.mongePoint = (↑(n + 1) / ↑(n - 1)) • (Finset.centroid ℝ Finset.univ s.points -ᵥ s.circumcenter) +ᵥ s.circumcenter
-- Mathlib.Topology.Bases
TopologicalSpace.exists_countable_basis : ∀ (α : Type u) [t : TopologicalSpace α] [SecondCountableTopology α],
  ∃ b, b.Countable ∧ ∅ ∉ b ∧ TopologicalSpace.IsTopologicalBasis b
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_restrict_apply_self : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Set α), (μ.restrict s).real s = μ.real s
-- Batteries.Data.AssocList
/-- `O(n)`. Replace the first entry `a', b` in the list
with key equal to `a` to have key `a` and value `f a' b`.
 -/
Batteries.AssocList.modify : {α : Type u_1} → {β : Type u_2} → [BEq α] → α → (α → β → β) → Batteries.AssocList α β → Batteries.AssocList α β
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.size_le_size_insert : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α} {v : β k}, m.size ≤ (m.insert k v).size
-- Mathlib.Analysis.Analytic.Basic
AnalyticAt.continuousAt : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E},
  AnalyticAt 𝕜 f x → ContinuousAt f x
-- Batteries.Data.AssocList
_private.Batteries.Data.AssocList.0.cond.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match true with
    | true => h_1 ()
    | false => h_2 ()) =
    h_1 ()
-- Mathlib.Algebra.Group.Basic
/-- **Alias** of `additive_of_symm_of_total`. -/
additive_of_symmetric_of_isTotal : ∀ {α : Type u_1} {β : Type u_2} [inst : AddMonoid β] (p r : α → α → Prop) [Std.Total r] (f : α → α → β) [Std.Symm p],
  (∀ {a b : α}, p a b → f a b + f b a = 0) →
    (∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b + f b c) →
      ∀ {a b c : α}, p a b → p b c → p a c → f a c = f a b + f b c
-- Mathlib.Analysis.Complex.Basic
Complex.re_eq_ofReal_of_isSelfAdjoint : ∀ {x : ℂ} {y : ℝ}, IsSelfAdjoint x → (x.re = y ↔ x = ↑y)
-- Mathlib.Data.Set.Sups
Set.sups_inter_subset_left : ∀ {α : Type u_2} [inst : SemilatticeSup α] {s₁ s₂ t : Set α}, (s₁ ∩ s₂) ⊻ t ⊆ s₁ ⊻ t ∩ s₂ ⊻ t
-- Mathlib.Algebra.Regular.Basic
/-- If `R` is an additive monoid, an element in `add_units R` is add-regular.  -/
AddUnits.isAddRegular : ∀ {R : Type u_1} [inst : AddMonoid R] (a : AddUnits R), IsAddRegular ↑a
-- Mathlib.Algebra.Module.Congruence.Defs
ModuleCon.mk.sizeOf_spec : ∀ {S : Type u_2} {M : Type u_3} [inst : Add M] [inst_1 : SMul S M] [inst_2 : SizeOf S] [inst_3 : SizeOf M]
  (toAddCon : AddCon M) (smul : ∀ (s : S) {x y : M}, toAddCon.toSetoid x y → toAddCon.toSetoid (s • x) (s • y)),
  sizeOf { toAddCon := toAddCon, smul := smul } = 1 + sizeOf toAddCon
-- Aesop.Forward.PremiseIndex
Aesop.instToStringPremiseIndex : ToString Aesop.PremiseIndex
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.hasTensor_of_iso : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] {X₁ X₂ Y₁ Y₂ : CategoryTheory.GradedObject I C} (e₁ : X₁ ≅ Y₁)
  (e₂ : X₂ ≅ Y₂) [X₁.HasTensor X₂], Y₁.HasTensor Y₂
-- Mathlib.AlgebraicTopology.SimplicialSet.Nerve
CategoryTheory.nerve.δ₂_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (x : CategoryTheory.ComposableArrows C 2),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (CategoryTheory.nerve C) 0)) x =
    CategoryTheory.ComposableArrows.mk₁
      (x.map' 1 2 CategoryTheory.nerve.δ₂_two._proof_3 CategoryTheory.nerve.δ₂_zero._proof_1)
-- Mathlib.Algebra.Homology.Embedding.Basic
ComplexShape.Embedding.instIsTruncGEOpOfIsTruncLE : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [e.IsTruncLE],
  e.op.IsTruncGE
-- Mathlib.RingTheory.LaurentSeries
/-- An abbreviation for the `X`-adic completion of `K⟮X⟯`  -/
LaurentSeries.RatFuncAdicCompl : (K : Type u_2) → [Field K] → Type u_2
-- Lean.DocString.Parser
Lean.Doc.Parser.BlockCtxt.mk.inj : ∀ {minIndent : ℕ} {maxDirective : Option ℕ} {inLists : List Lean.Doc.Parser.InList} {docStartPosition : Lean.Position}
  {baseColumn minIndent_1 : ℕ} {maxDirective_1 : Option ℕ} {inLists_1 : List Lean.Doc.Parser.InList}
  {docStartPosition_1 : Lean.Position} {baseColumn_1 : ℕ},
  { minIndent := minIndent, maxDirective := maxDirective, inLists := inLists, docStartPosition := docStartPosition,
        baseColumn := baseColumn } =
      { minIndent := minIndent_1, maxDirective := maxDirective_1, inLists := inLists_1,
        docStartPosition := docStartPosition_1, baseColumn := baseColumn_1 } →
    minIndent = minIndent_1 ∧
      maxDirective = maxDirective_1 ∧
        inLists = inLists_1 ∧ docStartPosition = docStartPosition_1 ∧ baseColumn = baseColumn_1
-- Mathlib.Data.PNat.Xgcd
PNat.XgcdType.reduce.eq_def : ∀ (u : PNat.XgcdType), u.reduce = if x : u.r = 0 then u.finish else u.step.reduce.flip
-- Mathlib.RingTheory.TensorProduct.Basic
TensorProduct.instStarRing : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : NonUnitalNonAssocSemiring A] →
          [inst_2 : NonUnitalNonAssocSemiring B] →
            [inst_3 : Module R A] →
              [inst_4 : Module R B] →
                [inst_5 : SMulCommClass R A A] →
                  [inst_6 : SMulCommClass R B B] →
                    [inst_7 : IsScalarTower R A A] →
                      [inst_8 : IsScalarTower R B B] →
                        [inst_9 : StarRing R] →
                          [inst_10 : StarRing A] →
                            [inst_11 : StarRing B] →
                              [StarModule R A] → [StarModule R B] → StarRing (TensorProduct R A B)
-- Init.Data.SInt.Lemmas
Int32.ofIntLE_add : ∀ {a b : ℤ} {hab₁ : Int32.minValue.toInt ≤ a + b} {hab₂ : a + b ≤ Int32.maxValue.toInt},
  Int32.ofIntLE (a + b) hab₁ hab₂ = Int32.ofInt a + Int32.ofInt b
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.mapMonNatIso_inv_app_hom : ∀ {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]
  {F F' : CategoryTheory.Functor C D} [inst_4 : F.LaxMonoidal] [inst_5 : F'.LaxMonoidal] (e : F ≅ F')
  [inst_6 : CategoryTheory.NatTrans.IsMonoidal e.hom] (X : CategoryTheory.Mon C),
  ((CategoryTheory.Functor.mapMonNatIso e).inv.app X).hom = e.inv.app X.X
-- Mathlib.Data.Finset.Sups
Finset.compls_compls : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (s : Finset α), s.compls.compls = s
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
IsBoundedLinearMap.snd : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : Module 𝕜 F], IsBoundedLinearMap 𝕜 fun x => x.2
-- Init.Data.String.Lemmas.Pattern.Split.Basic
String.toList_split_empty : ∀ {ρ : Type} (pat : ρ) [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] {σ : String.Slice → Type}
  [inst_2 : String.Slice.Pattern.ToForwardSearcher pat σ]
  [inst_3 : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)]
  [inst_4 : ∀ (s : String.Slice), Std.Iterators.Finite (σ s) Id]
  [String.Slice.Pattern.Model.LawfulToForwardSearcherModel pat], List.map String.Slice.copy ("".split pat).toList = [""]
-- Mathlib.CategoryTheory.Localization.Prod
/-- If `L₁ : C₁ ⥤ D₁` and `L₂ : C₂ ⥤ D₂` are localization functors
for `W₁ : MorphismProperty C₁` and `W₂ : MorphismProperty C₂` respectively,
and if both `W₁` and `W₂` contain identities, then the product
functor `L₁.prod L₂ : C₁ × C₂ ⥤ D₁ × D₂` is a localization functor for `W₁.prod W₂`.  -/
CategoryTheory.Functor.IsLocalization.prod : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₃} {D₂ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} D₁]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D₂] (L₁ : CategoryTheory.Functor C₁ D₁)
  (W₁ : CategoryTheory.MorphismProperty C₁) (L₂ : CategoryTheory.Functor C₂ D₂)
  (W₂ : CategoryTheory.MorphismProperty C₂) [W₁.ContainsIdentities] [W₂.ContainsIdentities] [L₁.IsLocalization W₁]
  [L₂.IsLocalization W₂], (L₁.prod L₂).IsLocalization (W₁.prod W₂)
-- Init.Grind.Offset
Lean.Grind.Nat.lo_eq_true_of_lo : ∀ (u v k₁ k₂ : ℕ), Lean.Grind.isLE k₂ k₁ = true → u + k₁ ≤ v → (u + k₂ ≤ v) = True
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.HasAbsLeftKanExtension.toHasLeftKanExtension : ∀ {B : Type u} {inst : CategoryTheory.Bicategory B} {a b c : B} {f : a ⟶ b} {g : a ⟶ c}
  [self : CategoryTheory.Bicategory.HasAbsLeftKanExtension f g], CategoryTheory.Bicategory.HasLeftKanExtension f g
-- Mathlib.MeasureTheory.Integral.Average
/-- **First moment method**. An integrable function is greater than its integral on a set of
positive measure.  -/
MeasureTheory.measure_integral_le_pos : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ}
  [MeasureTheory.IsProbabilityMeasure μ], MeasureTheory.Integrable f μ → 0 < μ {x | ∫ (a : α), f a ∂μ ≤ f x}
-- Mathlib.Algebra.Notation.Defs
/-- Type class for the `/ₛ` notation.  -/
SDiv : outParam (Type u_1) → Type u_2 → Type (max u_1 u_2)
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.Quotient.mkₐ_eq_mk : ∀ (R₁ : Type u_1) {A : Type u_3} [inst : CommSemiring R₁] [inst_1 : Ring A] [inst_2 : Algebra R₁ A] (I : Ideal A)
  [inst_3 : I.IsTwoSided], ⇑(Ideal.Quotient.mkₐ R₁ I) = ⇑(Ideal.Quotient.mk I)
-- Mathlib.Analysis.Analytic.Constructions
AnalyticWithinAt.restrictScalars : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {𝕜' : Type u_9}
  [inst_5 : NontriviallyNormedField 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜'] [inst_7 : NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E]
  [inst_9 : NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {f : E → F} {x : E} {s : Set E},
  AnalyticWithinAt 𝕜' f s x → AnalyticWithinAt 𝕜 f s x
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum_of_ac : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α} [MeasurableConstSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G]
  {ν : MeasureTheory.Measure α},
  MeasureTheory.IsFundamentalDomain G s μ →
    ν.AbsolutelyContinuous μ → ∀ (f : α → ENNReal), ∫⁻ (x : α), f x ∂ν = ∑' (g : G), ∫⁻ (x : α) in g • s, f x ∂ν
-- Mathlib.Topology.Compactness.LocallyCompact
compact_basis_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X] [LocallyCompactSpace X] (x : X),
  (nhds x).HasBasis (fun s => s ∈ nhds x ∧ IsCompact s) fun s => s
-- Mathlib.CategoryTheory.EquivalenceRelation
/-- Given an effective equivalence relation structure `e` on `p₁, p₂ : R ⟶ A`, the morphism
`e.π : A ⟶ e.B` makes `e.B` a coequalizer of `p₁` and `p₂`.  -/
CategoryTheory.EffectiveEquivalenceRelation.isCoequalizer : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {R A : C} →
      (p₁ p₂ : R ⟶ A) →
        (e : CategoryTheory.EffectiveEquivalenceRelation p₁ p₂) →
          CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ e.π ⋯)
-- Mathlib.RingTheory.Artinian.Module
IsArtinian.range_smul_pow_stabilizes : ∀ {R : Type u_1} (M : Type u_2) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [IsArtinian R M] (r : R), ∃ n, ∀ (m : ℕ), n ≤ m → (r ^ n • LinearMap.id).range = (r ^ m • LinearMap.id).range
-- Mathlib.Algebra.BigOperators.Finprod
finsum_cond_eq_sum_of_cond_iff : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] (f : α → M) {p : α → Prop} {t : Finset α},
  (∀ {x : α}, f x ≠ 0 → (p x ↔ x ∈ t)) → ∑ᶠ (i : α) (_ : p i), f i = ∑ i ∈ t, f i
-- Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
CategoryTheory.PreOneHypercover.IsStronglySeparatedFor.arrowsCompatible : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : C} {E : CategoryTheory.PreOneHypercover X}
  {F : CategoryTheory.Functor Cᵒᵖ (Type u_2)},
  E.IsStronglySeparatedFor F →
    ∀ (x : (i : E.I₀) → F.obj (Opposite.op (E.X i))),
      (∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
          (CategoryTheory.ConcreteCategory.hom (F.map (E.p₁ k).op)) (x i) =
            (CategoryTheory.ConcreteCategory.hom (F.map (E.p₂ k).op)) (x j)) →
        CategoryTheory.Presieve.Arrows.Compatible F E.f x
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Subgroup.mem_zpowers_iff : ∀ {G : Type u_1} [inst : Group G] {g h : G}, h ∈ Subgroup.zpowers g ↔ ∃ k, g ^ k = h
-- Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
CategoryTheory.ObjectProperty.epiModSerre_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsSerreClass] {X Y : C} (f : X ⟶ Y),
  P.epiModSerre f ↔ P (CategoryTheory.Limits.cokernel f)
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.bot_eq_zero : ⊥ = 0
-- Mathlib.Data.QPF.Multivariate.Constructions.Prj
/-- The projection `i` functor  -/
MvQPF.Prj : {n : ℕ} → Fin2 n → TypeVec.{u} n → Type u
-- Init.SimpLemmas
and_false : ∀ (p : Prop), (p ∧ False) = False
-- Mathlib.LinearAlgebra.FreeModule.Basic
Module.End.mem_submonoidCenter_iff : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M]
  {f : Module.End R M},
  f ∈ Submonoid.center (Module.End R M) ↔ ∃ α, ∃ (hα : α ∈ Submonoid.center R), f = Module.End.smulLeft α hα
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.LeftHomologyData.mapLeftHomologyIso_eq : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} (hl : S.LeftHomologyData)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : S.HasLeftHomology]
  [inst_6 : F.PreservesLeftHomologyOf S],
  S.mapLeftHomologyIso F = (hl.map F).leftHomologyIso ≪≫ F.mapIso hl.leftHomologyIso.symm
-- Init.Prelude
/-- The `OfNat.ofNat` function is automatically inserted by the parser when
the user writes a numeric literal like `1 : α`. Implementations of this
typeclass can therefore customize the behavior of `n : α` based on `n` and
`α`.  -/
OfNat.ofNat : {α : Type u} → (x : ℕ) → [self : OfNat α x] → α
-- Mathlib.Algebra.Homology.Embedding.Basic
ComplexShape.Embedding.IsTruncLE.mk : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {e : c.Embedding c'}
  [toIsRelIff : e.IsRelIff], (∀ {i' : ι'} {j : ι}, c'.Rel i' (e.f j) → ∃ i, e.f i = i') → e.IsTruncLE
-- Init.Data.String.PosRaw
String.Pos.Raw.increaseBy_zero : ∀ {p : String.Pos.Raw}, p.increaseBy 0 = p
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙ_smul_id : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] {S : Type u_3}
  [inst_12 : SMulZeroClass S R] [ContinuousConstSMul S R] [inst_14 : SMulZeroClass S A] [IsScalarTower S R A]
  [IsScalarTower S R (R → R)] (s : S) (a : A), autoParam (p a) cfcₙ_smul_id._auto_1 → cfcₙ (fun x => s • x) a = s • a
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.contains_ofList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List ((a : α) × β a)} {k : α}, (Std.ExtDHashMap.ofList l).contains k = (List.map Sigma.fst l).contains k
-- Mathlib.Combinatorics.SimpleGraph.Prod
SimpleGraph.Iso.boxProdSumDistrib_toEquiv : ∀ {V : Type u_4} {W₁ : Type u_8} {W₂ : Type u_9} (G : SimpleGraph V) (H₁ : SimpleGraph W₁) (H₂ : SimpleGraph W₂),
  (SimpleGraph.Iso.boxProdSumDistrib G H₁ H₂).toEquiv = Equiv.prodSumDistrib V W₁ W₂
-- Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Subalgebra.rTensorBot_tmul : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S]
  {A : Subalgebra R S} (x : R) (a : ↥A), A.rTensorBot (a ⊗ₜ[R] (algebraMap R ↥⊥) x) = x • a
-- Lean.Message
/-- A widget instance.

In `ofWidget wi alt`,
the nested message `alt` should approximate the contents of the widget
without itself using `ofWidget wi _`.
This is used as fallback in environments that cannot display user widgets.
`alt` may nest any structured message,
for example `ofGoal` to approximate a tactic state widget,
and, if necessary, even other widget instances
(for which approximations are computed recursively).

Note that unlike with `Widget.savePanelWidgetInfo`,
the infoview will not pass any additional props to the widget instance.  -/
Lean.MessageData.ofWidget : Lean.Widget.WidgetInstance → Lean.MessageData → Lean.MessageData
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.uIcc_self : ∀ {α : Type u_1} [inst : Lattice α] {a : α}, Set.uIcc a a = {a}
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
SummationFilter.NeBot.mk : ∀ {β : Type u_2} {L : SummationFilter β}, L.filter.NeBot → L.NeBot
-- Mathlib.CategoryTheory.Bicategory.Yoneda
/-- Version of `Bicategory.postcomposing` viewed in the bicategory `Cat`.  -/
CategoryTheory.Bicategory.postcomposingCat : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    (a b c : B) → CategoryTheory.Functor (b ⟶ c) (CategoryTheory.Cat.of (a ⟶ b) ⟶ CategoryTheory.Cat.of (a ⟶ c))
-- Mathlib.MeasureTheory.Function.AEEqFun.DomAct
DomMulAct.instDistribMulActionAEEqFun : {M : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : MeasurableSpace α] →
        {μ : MeasureTheory.Measure α} →
          [inst_1 : TopologicalSpace β] →
            [inst_2 : Monoid M] →
              [inst_3 : MulAction M α] →
                [MeasurableConstSMul M α] →
                  [MeasureTheory.SMulInvariantMeasure M α μ] →
                    [inst_6 : AddMonoid β] → [inst_7 : ContinuousAdd β] → DistribMulAction Mᵈᵐᵃ (α →ₘ[μ] β)
-- Mathlib.Order.Hom.Lattice
LatticeHom.coe_snd : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β], ⇑LatticeHom.snd = Prod.snd
-- Mathlib.Topology.Baire.Lemmas
/-- If `f` is an open quotient map and `X` is Baire, then `Y` is Baire.  -/
IsOpenQuotientMap.baireSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [BaireSpace X] {Y : Type u_4} [inst_2 : TopologicalSpace Y] {f : X → Y},
  IsOpenQuotientMap f → BaireSpace Y
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instAddRightCancelMonoid.eq_1 : ∀ {α : Type u_1} [inst : AddRightCancelMonoid α],
  OrderDual.instAddRightCancelMonoid = { toAddMonoid := OrderDual.instAddMonoid, toIsRightCancelAdd := ⋯ }
-- Init.GrindInstances.ToInt
Lean.Grind.instSubIntIi : Lean.Grind.ToInt.Sub ℤ Lean.Grind.IntInterval.ii
-- Std.Data.DTreeMap.Raw.Iterator
Std.DTreeMap.Raw.values.eq_1 : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} (t : Std.DTreeMap.Raw α (fun x => β) cmp),
  t.values = t.inner.values
-- Mathlib.Algebra.Category.Grp.LeftExactFunctor
AddCommGrpCat.leftExactFunctorForgetEquivalence.inverseAux.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteBiproducts C],
  AddCommGrpCat.leftExactFunctorForgetEquivalence.inverseAux =
    AddCommGrpCat.leftExactFunctorForgetEquivalence.inverseAux
-- Mathlib.Data.Finset.Preimage
Finset.preimage_inter : ∀ {α : Type u} {β : Type v} [inst : DecidableEq α] [inst_1 : DecidableEq β] {f : α → β} {s t : Finset β}
  (hs : Set.InjOn f (f ⁻¹' ↑s)) (ht : Set.InjOn f (f ⁻¹' ↑t)), (s ∩ t).preimage f ⋯ = s.preimage f hs ∩ t.preimage f ht
-- Mathlib.Algebra.Order.Archimedean.Hom
/-- There is at most one ordered ring isomorphism between an archimedean linear ordered field and a
linear ordered field.  -/
OrderRingIso.subsingleton_left : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : Field β] [inst_3 : LinearOrder β]
  [IsStrictOrderedRing α] [Archimedean α], Subsingleton (α ≃+*o β)
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.completeMultipartiteGraph.not_cliqueFree_of_le_card : ∀ {n : ℕ} {ι : Type u_3} (V : ι → Type u_4) [inst : Fintype ι] (f : (i : ι) → V i),
  n ≤ Fintype.card ι → ¬(SimpleGraph.completeMultipartiteGraph V).CliqueFree n
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.Hom.mk.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M₁ M₂ : PresheafOfModules R} (app app_1 : (X : Cᵒᵖ) → M₁.obj X ⟶ M₂.obj X) (e_app : app = app_1)
  (naturality :
    ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
      CategoryTheory.CategoryStruct.comp (M₁.map f)
          ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (app Y)) =
        CategoryTheory.CategoryStruct.comp (app X) (M₂.map f)),
  { app := app, naturality := naturality } = { app := app_1, naturality := ⋯ }
-- Init.Data.Int.DivMod.Lemmas
Int.sub_emod_left : ∀ (a b : ℤ), (a - b) % a = -b % a
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.primrec₂_pair : Primrec₂ Nat.Partrec.Code.pair
-- Mathlib.LinearAlgebra.Span.Basic
/-- An induction principle for elements of `⨆ i, p i`.
If `C` holds for `0` and all elements of `p i` for all `i`, and is preserved under addition,
then it holds for all elements of the supremum of `p`.  -/
Submodule.iSup_induction : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Sort u_8}
  (p : ι → Submodule R M) {motive : M → Prop} {x : M},
  x ∈ ⨆ i, p i →
    (∀ (i : ι), ∀ x ∈ p i, motive x) → motive 0 → (∀ (x y : M), motive x → motive y → motive (x + y)) → motive x
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- The relation `IsContained A B`, `A ⊑ B` says that `B` contains a copy of `A`.

This is equivalent to the existence of an isomorphism from `A` to a subgraph of `B`.  -/
SimpleGraph.IsContained : {α : Type u_4} → {β : Type u_5} → SimpleGraph α → SimpleGraph β → Prop
-- Mathlib.Topology.Order
isOpen_implies_isOpen_iff : ∀ {α : Type u_1} {t₁ t₂ : TopologicalSpace α}, (∀ (s : Set α), IsOpen s → IsOpen s) ↔ t₂ ≤ t₁
-- Init.Data.Vector.Attach
Vector.mem_unattach : ∀ {α : Type u_1} {n : ℕ} {p : α → Prop} {xs : Vector { x // p x } n} {a : α}, a ∈ xs.unattach ↔ ∃ (h : p a), ⟨a, h⟩ ∈ xs
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- Show that the functor given by `leftAdjointOfEquiv` is indeed left adjoint to `G`. Dual
to `adjunctionOfEquivRight`.  -/
CategoryTheory.Adjunction.adjunctionOfEquivLeft : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {G : CategoryTheory.Functor D C} →
          {F_obj : C → D} →
            (e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)) →
              (he :
                  ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y),
                    (e X Y') (CategoryTheory.CategoryStruct.comp h g) =
                      CategoryTheory.CategoryStruct.comp ((e X Y) h) (G.map g)) →
                CategoryTheory.Adjunction.leftAdjointOfEquiv e he ⊣ G