mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.size_ofList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List (α × β)},
  List.Pairwise (fun a b => (a.1 == b.1) = false) l → (Std.ExtDHashMap.Const.ofList l).size = l.length
-- Mathlib.Probability.Kernel.CondDistrib
ProbabilityTheory.condDistrib_congr_right : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_3 : MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β} {X' : α → β},
  X =ᵐ[μ] X' → ProbabilityTheory.condDistrib Y X μ = ProbabilityTheory.condDistrib Y X' μ
-- Lean.Server.AsyncList
Lean.AsyncList.brecOn_3.eq : ∀ {ε : Type u} {α : Type v} {motive_1 : Lean.AsyncList ε α → Sort u_1}
  {motive_2 : Lean.Server.ServerTask (Except ε (Lean.AsyncList ε α)) → Sort u_1}
  {motive_3 : Task (Except ε (Lean.AsyncList ε α)) → Sort u_1} {motive_4 : Except ε (Lean.AsyncList ε α) → Sort u_1}
  (t : Except ε (Lean.AsyncList ε α)) (F_1 : (t : Lean.AsyncList ε α) → t.below → motive_1 t)
  (F_2 : (t : Lean.Server.ServerTask (Except ε (Lean.AsyncList ε α))) → Lean.AsyncList.below_1 t → motive_2 t)
  (F_3 : (t : Task (Except ε (Lean.AsyncList ε α))) → Lean.AsyncList.below_2 t → motive_3 t)
  (F_4 : (t : Except ε (Lean.AsyncList ε α)) → Lean.AsyncList.below_3 t → motive_4 t),
  Lean.AsyncList.brecOn_3 t F_1 F_2 F_3 F_4 = F_4 t (Lean.AsyncList.brecOn_3.go t F_1 F_2 F_3 F_4).2
-- Mathlib.Control.Functor
Functor.Const.lawfulFunctor : ∀ {γ : Type u_1}, LawfulFunctor (Functor.Const γ)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.opcyclesIsoX₂_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasRightHomology] (hf : S.f = 0),
  (S.opcyclesIsoX₂ hf).inv = S.pOpcycles
-- Mathlib.CategoryTheory.Abelian.Refinements
CategoryTheory.ShortComplex.comp_pOpcycles_eq_zero_iff_up_to_refinements : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S : CategoryTheory.ShortComplex C} {A : C} (x₂ : A ⟶ S.X₂),
  CategoryTheory.CategoryStruct.comp x₂ S.pOpcycles = 0 ↔
    ∃ A' π,
      ∃ (_ : CategoryTheory.Epi π),
        ∃ x₁, CategoryTheory.CategoryStruct.comp π x₂ = CategoryTheory.CategoryStruct.comp x₁ S.f
-- Lean.Meta.Tactic.Grind.AC.Seq
_private.Lean.Meta.Tactic.Grind.AC.Seq.0.Lean.Grind.AC.Seq.startsWith.match_1.eq_4 : ∀ (motive : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Sort u_1) (x : Lean.Grind.AC.Var) (s₂ : Lean.Grind.AC.Seq)
  (y : Lean.Grind.AC.Var) (s₁ : Lean.Grind.AC.Seq)
  (h_1 : (x y : Lean.Grind.AC.Var) → motive (Lean.Grind.AC.Seq.var x) (Lean.Grind.AC.Seq.var y))
  (h_2 :
    (x y : Lean.Grind.AC.Var) → (s : Lean.Grind.AC.Seq) → motive (Lean.Grind.AC.Seq.var x) (Lean.Grind.AC.Seq.cons y s))
  (h_3 :
    (x : Lean.Grind.AC.Var) →
      (s : Lean.Grind.AC.Seq) →
        (x_1 : Lean.Grind.AC.Var) → motive (Lean.Grind.AC.Seq.cons x s) (Lean.Grind.AC.Seq.var x_1))
  (h_4 :
    (x : Lean.Grind.AC.Var) →
      (s₂ : Lean.Grind.AC.Seq) →
        (y : Lean.Grind.AC.Var) →
          (s₁ : Lean.Grind.AC.Seq) → motive (Lean.Grind.AC.Seq.cons x s₂) (Lean.Grind.AC.Seq.cons y s₁)),
  (match Lean.Grind.AC.Seq.cons x s₂, Lean.Grind.AC.Seq.cons y s₁ with
    | Lean.Grind.AC.Seq.var x, Lean.Grind.AC.Seq.var y => h_1 x y
    | Lean.Grind.AC.Seq.var x, Lean.Grind.AC.Seq.cons y s => h_2 x y s
    | Lean.Grind.AC.Seq.cons x s, Lean.Grind.AC.Seq.var x_1 => h_3 x s x_1
    | Lean.Grind.AC.Seq.cons x s₂, Lean.Grind.AC.Seq.cons y s₁ => h_4 x s₂ y s₁) =
    h_4 x s₂ y s₁
-- Mathlib.Algebra.Group.Action.Sum
Sum.vadd_swap : ∀ {M : Type u_1} {α : Type u_3} {β : Type u_4} [inst : VAdd M α] [inst_1 : VAdd M β] (a : M) (x : α ⊕ β),
  (a +ᵥ x).swap = a +ᵥ x.swap
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
/-- Given `SlashInvariantForm`'s `f i` of weight `k`, define the form which as a
function is a product of those indexed by `s : Finset ι` with weight `#s * k`.  -/
SlashInvariantForm.prodEqualWeights : {ι : Type} →
  {s : Finset ι} →
    {k : ℤ} →
      {Γ : Subgroup (GL (Fin 2) ℝ)} →
        [Γ.HasDetPlusMinusOne] → (ι → SlashInvariantForm Γ k) → SlashInvariantForm Γ (↑s.card * k)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.algHom_ext' : ∀ {k : Type u_1} {G : Type u_2} [inst : Monoid G] [inst_1 : CommSemiring k] {A : Type u_3} [inst_2 : Semiring A]
  [inst_3 : Algebra k A] [inst_4 : MulSemiringAction G k] [inst_5 : SMulCommClass G k k]
  ⦃φ₁ φ₂ : SkewMonoidAlgebra k G →ₐ[k] A⦄,
  (↑φ₁).comp (SkewMonoidAlgebra.of k G) = (↑φ₂).comp (SkewMonoidAlgebra.of k G) → φ₁ = φ₂
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDerivWithin_comp_neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {s : Set 𝕜} {f : 𝕜 → F} (a : 𝕜),
  iteratedDerivWithin n (fun x => f (-x)) s a = (-1) ^ n • iteratedDerivWithin n f (-s) (-a)
-- Mathlib.Order.Interval.Set.LinearOrder
/-- **Alias** of `Set.Ici_sdiff_Ici`. -/
Set.Ici_diff_Ici : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Ici a \ Set.Ici b = Set.Ico a b
-- Mathlib.Topology.Maps.Basic
Topology.IsOpenEmbedding.map_nhds_eq : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Topology.IsOpenEmbedding f → ∀ (x : X), Filter.map f (nhds x) = nhds (f x)
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.openCoverOfIsOpenCover_X : ∀ {s : Type u_1} (X : AlgebraicGeometry.Scheme) (U : s → X.Opens) (hU : TopologicalSpace.IsOpenCover U) (i : s),
  (X.openCoverOfIsOpenCover U hU).X i = ↑(U i)
-- Mathlib.Algebra.Category.ModuleCat.FilteredColimits
ModuleCat.FilteredColimits.forget_reflectsFilteredColimits : ∀ {R : Type u} [inst : Ring R], CategoryTheory.Limits.ReflectsFilteredColimits (CategoryTheory.forget (ModuleCat R))
-- Std.Data.DHashMap.Raw
/-- Erases multiple keys from the hash map by iterating over the given collection and calling
`erase` on each key. The values in the collection are ignored; only the keys are used for erasure.
If the same key appears multiple times in the collection, subsequent erasures have no effect after
the first one removes the key.
 -/
Std.DHashMap.Raw.eraseManyEntries : {α : Type u} →
  {β : α → Type v} →
    [BEq α] →
      [Hashable α] → {ρ : Type w} → [ForIn Id ρ ((a : α) × β a)] → Std.DHashMap.Raw α β → ρ → Std.DHashMap.Raw α β
-- Mathlib.Analysis.Polynomial.MahlerMeasure
Polynomial.logMahlerMeasure_const : ∀ (z : ℂ), (Polynomial.C z).logMahlerMeasure = Real.log ‖z‖
-- Mathlib.RingTheory.Polynomial.DegreeLT
Polynomial.degreeLT.addLinearEquiv_symm_apply_inr_basis : ∀ {R : Type u_1} [inst : Semiring R] {m n : ℕ} (j : Fin n),
  (Polynomial.degreeLT.addLinearEquiv R m n).symm
      ((LinearMap.inr R ↥(Polynomial.degreeLT R m) ↥(Polynomial.degreeLT R n)) ((Polynomial.degreeLT.basis R n) j)) =
    (Polynomial.degreeLT.basis R (m + n)) (Fin.natAdd m j)
-- Mathlib.Data.List.AList
AList.lookup_erase_ne : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a a' : α} {s : AList β},
  a ≠ a' → AList.lookup a (AList.erase a' s) = AList.lookup a s
-- Lean.Parser.Term
/-- In a function application, `..` notation inserts zero or more `_` placeholders.  -/
Lean.Parser.Term.ellipsis : Lean.Parser.Parser
-- Init.Data.UInt.Bitwise
UInt32.xor_assoc : ∀ (a b c : UInt32), a ^^^ b ^^^ c = a ^^^ (b ^^^ c)
-- Init.Data.Nat.Div.Lemmas
Nat.div_add_le_right : ∀ {z : ℕ}, 0 < z → ∀ (x y : ℕ), x / (y + z) ≤ x / z
-- Mathlib.Algebra.Category.Ring.Limits
/-- The chosen cone is a limit cone.
(Generally, you'll just want to use `limit.cone F`.)
 -/
RingCat.limitConeIsLimit : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J RingCat) →
      [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget RingCat)).sections] →
        CategoryTheory.Limits.IsLimit (RingCat.limitCone F)
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.toSubmodule_sSup : ∀ {R : Type u_2} {N : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid N] [inst_2 : TopologicalSpace N]
  [inst_3 : Module R N] [inst_4 : ContinuousAdd N] [inst_5 : ContinuousConstSMul R N] (S : Set (ClosedSubmodule R N)),
  ↑(sSup S) = ↑(⨆ s ∈ S, ↑s).closure
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.Parallel.vectorSpan_eq : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s₁ s₂ : Set P},
  (affineSpan k s₁).Parallel (affineSpan k s₂) → vectorSpan k s₁ = vectorSpan k s₂
-- Mathlib.Algebra.Order.Monoid.Units
AddUnits.instOrd.eq_1 : ∀ {α : Type u_1} [inst : AddMonoid α] [inst_1 : Ord α], AddUnits.instOrd = { compare := fun a b => compare ↑a ↑b }
-- Mathlib.Algebra.Homology.Localization
ComplexShape.QFactorsThroughHomotopy.areEqualizedByLocalization : ∀ {ι : Type u_3} {c : ComplexShape ι} {C : Type u_4} {inst : CategoryTheory.Category.{v_2, u_4} C}
  {inst_1 : CategoryTheory.Preadditive C} {inst_2 : CategoryTheory.CategoryWithHomology C}
  [self : c.QFactorsThroughHomotopy C] {K L : HomologicalComplex C c} {f g : K ⟶ L} (h : Homotopy f g),
  CategoryTheory.AreEqualizedByLocalization (HomologicalComplex.quasiIso C c) f g
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- A left homology map data for a morphism of short complexes induces
a right homology map data in the opposite category.  -/
CategoryTheory.ShortComplex.LeftHomologyMapData.op : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        {φ : S₁ ⟶ S₂} →
          {h₁ : S₁.LeftHomologyData} →
            {h₂ : S₂.LeftHomologyData} →
              CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂ →
                CategoryTheory.ShortComplex.RightHomologyMapData (CategoryTheory.ShortComplex.opMap φ) h₂.op h₁.op
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.Sheaf.isLocallySurjective_sheafToPresheaf_map_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w'}
  [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [inst_3 : CategoryTheory.ConcreteCategory A FA]
  {F₁ F₂ : CategoryTheory.Sheaf J A} (φ : F₁ ⟶ F₂),
  CategoryTheory.Presheaf.IsLocallySurjective J ((CategoryTheory.sheafToPresheaf J A).map φ) ↔
    CategoryTheory.Sheaf.IsLocallySurjective φ
-- Mathlib.Algebra.Order.Group.Abs
abs_sub_lt_iff : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] {a b c : G},
  |a - b| < c ↔ a - b < c ∧ b - a < c
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.forget_obj : ∀ (R : Type u) [inst : Semiring R] {M : SemimoduleCat R}, (CategoryTheory.forget (SemimoduleCat R)).obj M = ↑M
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsAddFundamentalDomain.iUnion_vadd_ae_eq : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α}, MeasureTheory.IsAddFundamentalDomain G s μ → ⋃ g, g +ᵥ s =ᵐ[μ] Set.univ
-- Init.Data.List.Lemmas
List.getElem?_replicate : ∀ {n : ℕ} {α : Type u_1} {a : α} {i : ℕ}, (List.replicate n a)[i]? = if i < n then some a else none
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- **Alias** of `CategoryTheory.Mod`.

---

A module object for a monoid object in a monoidal category acting on the
ambient category.  -/
CategoryTheory.Mod_ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (D : Type u₂) →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
            (A : C) → [CategoryTheory.MonObj A] → Type (max u₂ v₂)
-- Mathlib.Topology.Bornology.Basic
OrderDual.isBounded_preimage_ofDual : ∀ {α : Type u_2} [inst : Bornology α] {s : Set α}, Bornology.IsBounded (⇑OrderDual.ofDual ⁻¹' s) ↔ Bornology.IsBounded s
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.limitUnopIsoUnopColimit_hom_comp_ι_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) [inst_2 : CategoryTheory.Limits.HasColimit F] (j : Jᵒᵖ) {Z : C}
  (h : Opposite.unop (F.obj j) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitUnopIsoUnopColimit F).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j).unop h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F.unop (Opposite.unop j)) h
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.apply_pow_apply_eq_iff : ∀ {α : Type u_1} (f : Equiv.Perm α) (n : ℕ) {x : α}, f ((f ^ n) x) = (f ^ n) x ↔ f x = x
-- Init.Data.Range.Polymorphic.UpwardEnumerable
/-- There is no cyclic chain of successors.  -/
Std.PRange.LawfulUpwardEnumerable.ne_of_lt : ∀ {α : Type u} {inst : Std.PRange.UpwardEnumerable α} [self : Std.PRange.LawfulUpwardEnumerable α] (a b : α),
  Std.PRange.UpwardEnumerable.LT a b → a ≠ b
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.setToFun_of_le_map : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C C' : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) {β : Type u_7}
  {x : MeasurableSpace β} {μ' : MeasureTheory.Measure β} {φ : α → β} {T' : Set β → E →L[ℝ] F}
  (hT' : MeasureTheory.DominatedFinMeasAdditive μ' T' C') {f : β → E},
  MeasureTheory.Integrable (f ∘ φ) μ →
    MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map φ μ) →
      Measurable φ →
        μ' ≤ MeasureTheory.Measure.map φ μ →
          (∀ (s : Set β) (x_1 : E), MeasurableSet s → (T' s) x_1 = (T (φ ⁻¹' s)) x_1) →
            MeasureTheory.setToFun μ' T' hT' f = MeasureTheory.setToFun μ T hT (f ∘ φ)
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.toLinearMap_mapIsometry : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [inst : RCLike 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F]
  [inst_4 : InnerProductSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G]
  [inst_7 : NormedAddCommGroup H] [inst_8 : InnerProductSpace 𝕜 H] (f : E →ₗᵢ[𝕜] G) (g : F →ₗᵢ[𝕜] H),
  (TensorProduct.mapIsometry f g).toLinearMap = TensorProduct.map f.toLinearMap g.toLinearMap
-- Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure
Algebra.IsIntegral.isTranscendenceBasis_iff : ∀ {ι : Type u_1} (R : Type u_2) {A : Type u_4} {x : ι → A} (S : Type u_5) [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : CommRing A] [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A]
  [NoZeroDivisors S] [FaithfulSMul R S] [Algebra.IsIntegral R S], IsTranscendenceBasis R x ↔ IsTranscendenceBasis S x
-- Std.Sat.AIG.Relabel
Std.Sat.AIG.Entrypoint.relabel.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {β : Type} [inst_2 : Hashable β] [inst_3 : DecidableEq β]
  (r : α → β) (entry : Std.Sat.AIG.Entrypoint α),
  Std.Sat.AIG.Entrypoint.relabel r entry =
    { aig := Std.Sat.AIG.relabel r entry.aig,
      ref :=
        let __src := entry.ref;
        { gate := __src.gate, invert := __src.invert, hgate := ⋯ } }
-- Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
/-- **Alias** of `CategoryTheory.Functor.toPseudofunctor`.

---

A functor between two categories `C` and `D` can be lifted to a pseudofunctor between the
corresponding locally discrete bicategories.
 -/
CategoryTheory.Functor.toPseudoFunctor : {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] →
        CategoryTheory.Functor C D →
          CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete C) (CategoryTheory.LocallyDiscrete D)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.toAddMonoidHom.eq_1 : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N), f.toAddMonoidHom = { toFun := f.toFun, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Topology.Neighborhoods
isOpen_iff_mem_nhds : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsOpen s ↔ ∀ x ∈ s, s ∈ nhds x
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Multipliable.mul : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f g : β → α}
  {L : SummationFilter β} [ContinuousMul α], Multipliable f L → Multipliable g L → Multipliable (fun b => f b * g b) L
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.ext' : ∀ {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : Semiring C] [inst_6 : Algebra R C]
  [inst_7 : CommSemiring S] [inst_8 : Algebra S A] [inst_9 : Algebra R S] [inst_10 : Algebra S C]
  [inst_11 : IsScalarTower R S A] [IsScalarTower R S C] {g h : TensorProduct R A B →ₐ[S] C},
  (∀ (a : A) (b : B), g (a ⊗ₜ[R] b) = h (a ⊗ₜ[R] b)) → g = h
-- Mathlib.Algebra.Group.Nat.Even
Nat.two_dvd_ne_zero : ∀ {n : ℕ}, ¬2 ∣ n ↔ n % 2 = 1
-- Mathlib.RingTheory.Extension.Cotangent.Basis
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.toAlgHom_fhom : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type u_4}
  {P : Algebra.Generators R S ι} {σ : Type u_5} {b : Module.Basis σ S P.toExtension.Cotangent}
  (D : Algebra.Generators.PresentationOfFreeCotangent.Aux✝ P b),
  (Algebra.Generators.PresentationOfFreeCotangent.Aux.fhom✝ D).toAlgHom = AlgHom.id R P.Ring
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.toReal_neg_eq_neg_toReal_iff : ∀ {θ : Real.Angle}, (-θ).toReal = -θ.toReal ↔ θ ≠ ↑Real.pi
-- Init.Data.List.Lemmas
List.foldr_eq_foldrM : ∀ {α : Type u_1} {β : Type u_2} {f : α → β → β} {b : β} {l : List α},
  List.foldr f b l = (List.foldrM (fun x1 x2 => pure (f x1 x2)) b l).run
-- Mathlib.CategoryTheory.EquivalenceRelation
/-- An equivalence relation is a reflexive, symmetric and transitive relation.  -/
CategoryTheory.EquivalenceRelation : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → {R X : C} → (R ⟶ X) → (R ⟶ X) → Type (max u_1 v_1)
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.coe_star : ∀ (z : Complex.UnitClosedDisc), ↑(star z) = (starRingEnd ℂ) ↑z
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.mem₁ : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.Functor.IsDenseSubsite J₀ J F] {X : C}
  (data : F.OneHypercoverDenseData J₀ J X) (i₁ i₂ : data.I₀) {W : C} (p₁ : W ⟶ F.obj (data.X i₁))
  (p₂ : W ⟶ F.obj (data.X i₂)),
  CategoryTheory.CategoryStruct.comp p₁ (data.f i₁) = CategoryTheory.CategoryStruct.comp p₂ (data.f i₂) →
    data.toPreOneHypercover.sieve₁ p₁ p₂ ∈ J W
-- Mathlib.Analysis.Complex.Conformal
isConformalMap_complex_linear_conj : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedSpace ℂ E] {map : ℂ →L[ℂ] E},
  map ≠ 0 → IsConformalMap (ContinuousLinearMap.restrictScalars ℝ map ∘SL ↑Complex.conjCLE)
-- Mathlib.Analysis.Seminorm
/-- The ball of radius `r` at `x` with respect to seminorm `p` is the set of elements `y` with
`p (y - x) < r`.  -/
Seminorm.ball : {𝕜 : Type u_3} →
  {E : Type u_7} →
    [inst : SeminormedRing 𝕜] → [inst_1 : AddCommGroup E] → [inst_2 : SMul 𝕜 E] → Seminorm 𝕜 E → E → ℝ → Set E
-- Mathlib.Algebra.BigOperators.Finprod
MonoidHom.map_finprod_plift : ∀ {M : Type u_2} {N : Type u_3} {α : Sort u_4} [inst : CommMonoid M] [inst_1 : CommMonoid N] (f : M →* N) (g : α → M),
  Function.HasFiniteMulSupport (g ∘ PLift.down) → f (∏ᶠ (x : α), g x) = ∏ᶠ (x : α), f (g x)
-- Mathlib.Tactic.FunProp.Types
/-- `RefinedDiscrTree` is lazy, so we store the partially evaluated tree.  -/
Mathlib.Meta.FunProp.State.morTheorems : Mathlib.Meta.FunProp.State → Mathlib.Meta.FunProp.GeneralTheorems
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Trace the proof of the normalization.  -/
Mathlib.Tactic.BicategoryLike.traceProof : {ρ : Type} → Lean.Name → Lean.Expr → Mathlib.Tactic.BicategoryLike.CoherenceM ρ Unit
-- Mathlib.Data.W.Constructions
/-- The isomorphism from the `WType` of the naturals to the naturals  -/
WType.toNat : WType WType.Natβ → ℕ
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- When we have `h : w.IsEquiv v`, the image group (with zero) of `v` is
isomorphic to that of `w` via `h.orderMonoidIso`. Then the following diagram is commutative:
```
              ValueGroup₀ w
                ∧      |
       embed w /       |
              /        |
ValueGroupWithZero R   | h.orderMonoidIso
              \        |
       embed v \       |
                ∨      ∨
              ValueGroup₀ v
```
 -/
ValuativeRel.ValueGroupWithZero.orderMonoidIso_embed : ∀ {R : Type u_2} {Γ : Type u_3} [inst : Ring R] [inst_1 : ValuativeRel R] [inst_2 : LinearOrderedCommGroupWithZero Γ]
  (v : Valuation R Γ) [inst_3 : v.Compatible] {Γ' : Type u_4} [inst_4 : LinearOrderedCommGroupWithZero Γ']
  (w : Valuation R Γ') [inst_5 : w.Compatible] (x : ValuativeRel.ValueGroupWithZero R) (h : w.IsEquiv v),
  h.orderMonoidIso ((ValuativeRel.ValueGroupWithZero.embed w) x) = (ValuativeRel.ValueGroupWithZero.embed v) x
-- Mathlib.Analysis.Normed.Operator.Prod
/-- The operator norm of the first projection `E × F → E` is at most 1. (It is 0 if `E` is zero, so
the inequality cannot be improved without further assumptions.)  -/
ContinuousLinearMap.norm_fst_le : ∀ (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : SeminormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 F],
  ‖ContinuousLinearMap.fst 𝕜 E F‖ ≤ 1
-- Mathlib.GroupTheory.Congruence.Basic
/-- The product of an indexed collection of congruence relations.  -/
Con.pi : {ι : Type u_4} → {f : ι → Type u_5} → [inst : (i : ι) → Mul (f i)] → ((i : ι) → Con (f i)) → Con ((i : ι) → f i)
-- Mathlib.Algebra.Order.Hom.Lattice
Finite.iSup_eq_iSup_subtype : ∀ {ι : Type u_1} {K : Type u_2} {M : Type u_3} {F : Type u_4} [Finite ι] [inst : Zero K] [inst_1 : Zero M]
  [inst_2 : ConditionallyCompleteLattice M] [inst_3 : FunLike F K M] [ZeroHomClass F K M] [NonnegHomClass F K M]
  {x : ι → K}, x ≠ 0 → ∀ {v : F}, ⨆ i, v (x i) = ⨆ i, v (x ↑i)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey!_le_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α}, k ∈ t → (cmp t.minKey! k).isLE = true
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.HasLeftHomology.condition : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C}
  {S : CategoryTheory.ShortComplex C} [self : S.HasLeftHomology], Nonempty S.LeftHomologyData