mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Join.Opposites
CategoryTheory.Join.inclRightCompOpEquivInverse_hom_app_op : ∀ {C : Type u₁} (D : Type u₂) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (c : C),
  (CategoryTheory.Join.inclRightCompOpEquivInverse C D).hom.app (Opposite.op c) =
    CategoryTheory.CategoryStruct.id (Opposite.op (CategoryTheory.Join.left c))
-- Aesop.Util.Basic
Aesop.SimpTheorems.addSimpEntry : Lean.Meta.SimpTheorems → Lean.Meta.SimpEntry → Lean.Meta.SimpTheorems
-- Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
instSMulCommClassMatrixFinOfNatNatProd : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_3} [inst_1 : DistribSMul S R] [SMulCommClass R S R],
  SMulCommClass (Matrix (Fin 2) (Fin 2) R) S (R × R)
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.StrongTrans.homCategory_comp_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {X Y Z : F ⟶ G} (Γ : CategoryTheory.Oplax.StrongTrans.Hom X Y)
  (Δ : CategoryTheory.Oplax.StrongTrans.Hom Y Z) (a : B),
  (CategoryTheory.CategoryStruct.comp Γ Δ).as.app a = CategoryTheory.CategoryStruct.comp (Γ.as.app a) (Δ.as.app a)
-- Mathlib.Topology.EMetricSpace.Defs
EMetric.dense_iff : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s : Set α}, Dense s ↔ ∀ (x : α), ∀ r > 0, (Metric.eball x r ∩ s).Nonempty
-- Mathlib.Tactic.GCongr.Core
/-- Insert a `GCongrLemma` in a collection of lemmas, making sure they are sorted by priority.  -/
Mathlib.Tactic.GCongr.addGCongrLemmaEntry : Mathlib.Tactic.GCongr.GCongrLemmas → Mathlib.Tactic.GCongr.GCongrLemma → Mathlib.Tactic.GCongr.GCongrLemmas
-- Mathlib.Topology.Order.LocalExtr
IsLocalExtrOn.isLocalExtr : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β} {s : Set α} {a : α},
  IsLocalExtrOn f s a → s ∈ nhds a → IsLocalExtr f a
-- Mathlib.Topology.Category.CompHaus.Basic
/-- An explicit limit cone for a functor `F : J ⥤ CompHaus`, defined in terms of
`TopCat.limitCone`.  -/
CompHaus.limitCone : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] → (F : CategoryTheory.Functor J CompHaus) → CategoryTheory.Limits.Cone F
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.pushforward_le_bind_of_mem : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (S : CategoryTheory.Presieve X)
  (R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → CategoryTheory.Sieve Y) (f : Y ⟶ X) (h : S f),
  CategoryTheory.Sieve.pushforward f (R h) ≤ CategoryTheory.Sieve.bind S R
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.biproduct.lift_desc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {J : Type}
  [inst_2 : Fintype J] {f : J → C} [inst_3 : CategoryTheory.Limits.HasBiproduct f] {T U : C} {g : (j : J) → T ⟶ f j}
  {h : (j : J) → f j ⟶ U},
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.lift g) (CategoryTheory.Limits.biproduct.desc h) =
    ∑ j, CategoryTheory.CategoryStruct.comp (g j) (h j)
-- Mathlib.LinearAlgebra.FiniteDimensional.Defs
/-- If a vector space is `FiniteDimensional`, all bases are indexed by a finite type  -/
FiniteDimensional.fintypeBasisIndex : {K : Type u} →
  {V : Type v} →
    [inst : DivisionRing K] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module K V] → {ι : Type u_1} → [FiniteDimensional K V] → Module.Basis ι K V → Fintype ι
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.Hom.ext_iff : ∀ {A B : CommMonCat} {x y : A.Hom B}, x = y ↔ x.hom' = y.hom'
-- Mathlib.Topology.Separation.Basic
/-- In a weakly locally compact R₁ space,
every compact set has an open neighborhood with compact closure.  -/
exists_isOpen_superset_and_isCompact_closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] [R1Space X] [WeaklyLocallyCompactSpace X] {K : Set X},
  IsCompact K → ∃ V, IsOpen V ∧ K ⊆ V ∧ IsCompact (closure V)
-- Mathlib.Data.Set.Insert
Set.insert_def : ∀ {α : Type u_1} (x : α) (s : Set α), insert x s = {y | y = x ∨ y ∈ s}
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.isEmpty_ofList : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α]
  {l : List ((a : α) × β a)}, (Std.DHashMap.ofList l).isEmpty = l.isEmpty
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.minEntry.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : (x : Std.DTreeMap.Internal.Impl α β) → x.isEmpty = false → Sort u_3)
  (size : ℕ) (k : α) (v : β k) (r : Std.DTreeMap.Internal.Impl α β)
  (x : (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r).isEmpty = false)
  (h_1 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (r : Std.DTreeMap.Internal.Impl α β) →
            (x : (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r).isEmpty = false) →
              motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β k_1) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r →
                      (r_1 : Std.DTreeMap.Internal.Impl α β) →
                        (h :
                            (Std.DTreeMap.Internal.Impl.inner size k v
                                  (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) r_1).isEmpty =
                              false) →
                          motive
                            (Std.DTreeMap.Internal.Impl.inner size k v
                              (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) r_1)
                            h),
  (match Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x with
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x => h_1 size k v r x
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) r_1,
      h_3 => h_2 size k v l size_1 k_1 v_1 l_1 r h r_1 h_3) =
    h_1 size k v r x
-- Lean.Elab.Tactic.Grind.Config
_private.Lean.Elab.Tactic.Grind.Config.0.Lean.Elab.Tactic.instEvalExprOrderConfig.evalExpr : Lean.Expr → Lean.MetaM Lean.Grind.OrderConfig
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_cast_Ioc : ∀ {m n : ℕ} (h : m = n) (i j : Fin n), Fin.cast h ⁻¹' Set.Ioc i j = Set.Ioc (Fin.cast ⋯ i) (Fin.cast ⋯ j)
-- Mathlib.Algebra.Module.Submodule.Invariant
Module.End.invtSubmodule.disjoint_mk_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (f : Module.End R M) {p q : Submodule R M} (hp : p ∈ f.invtSubmodule) (hq : q ∈ f.invtSubmodule),
  Disjoint ⟨p, hp⟩ ⟨q, hq⟩ ↔ Disjoint p q
-- Mathlib.Order.ScottContinuity
ScottContinuousOn.mono : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {D₁ D₂ : Set (Set α)} {f : α → β},
  D₁ ⊆ D₂ → ScottContinuousOn D₂ f → ScottContinuousOn D₁ f
-- Init.Prelude
/-- The empty type. It has no constructors.

Use `Empty.elim` in contexts where a value of type `Empty` is in scope.
 -/
Empty : Type
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs
Matrix.det_eq_prod_roots_charpoly_of_splits : ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {R : Type u_2} [inst_2 : CommRing R] {B : Matrix n n R}
  [inst_3 : IsDomain R], B.charpoly.Splits → B.det = B.charpoly.roots.prod
-- Mathlib.MeasureTheory.Function.LpSeminorm.Trim
MeasureTheory.limsup_trim : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) {f : α → ENNReal},
  Measurable f → Filter.limsup f (MeasureTheory.ae (μ.trim hm)) = Filter.limsup f (MeasureTheory.ae μ)
-- Mathlib.Topology.Category.CompHausLike.Basic
CompHausLike.instFullTopCatCompHausLikeToTop : ∀ (P : TopCat → Prop), (CompHausLike.compHausLikeToTop P).Full
-- Init.Data.Nat.Bitwise.Lemmas
Nat.two_pow_add_eq_or_of_lt : ∀ {i b : ℕ}, b < 2 ^ i → ∀ (a : ℕ), 2 ^ i * a + b = 2 ^ i * a ||| b
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.cast_divConst_mul_card : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {𝕜 : Type u_3} [inst_2 : Semifield 𝕜] [CharZero 𝕜]
  (A B : Finset G), ↑(A.divConst B) * ↑A.card = ↑(A / B).card
-- Batteries.Lean.Meta.UnusedNames
/-- Obtain `n` distinct names such that each name is unused in the current local
context and `suggestion` is a prefix of each name.
 -/
Lean.Meta.getUnusedUserNames : {m : Type → Type} → [Monad m] → [Lean.MonadLCtx m] → ℕ → Lean.Name → m (Array Lean.Name)
-- Mathlib.GroupTheory.GroupAction.Hom
MulDistribMulActionHom.map_sub : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} (A' : Type u_8) [inst_2 : Group A']
  [inst_3 : MulDistribMulAction M A'] (B' : Type u_9) [inst_4 : Group B'] [inst_5 : MulDistribMulAction N B']
  (f : A' →ₑ*[φ] B') (x y : A'), f (x / y) = f x / f y
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
uniformity_eq_comap_add_neg_nhds_zero_swapped : ∀ (Gᵣ : Type u_3) [inst : UniformSpace Gᵣ] [inst_1 : AddGroup Gᵣ] [IsRightUniformAddGroup Gᵣ],
  uniformity Gᵣ = Filter.comap (fun x => x.1 + -x.2) (nhds 0)
-- Mathlib.Algebra.Homology.HomologicalComplex
/-- The differential as a natural transformation between `eval`.  -/
HomologicalComplex.dNatTrans : {ι : Type u_1} →
  (V : Type u) →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
        (c : ComplexShape ι) → (i j : ι) → HomologicalComplex.eval V c i ⟶ HomologicalComplex.eval V c j
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.contains_insert_self : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α} {v : β k}, (m.insert k v).contains k = true
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
/-- Any descent of the zero morphism is homotopic to zero.  -/
CategoryTheory.InjectiveResolution.descHomotopyZero : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {Y Z : C} →
        {I : CategoryTheory.InjectiveResolution Y} →
          {J : CategoryTheory.InjectiveResolution Z} →
            (f : I.cocomplex ⟶ J.cocomplex) → CategoryTheory.CategoryStruct.comp I.ι f = 0 → Homotopy f 0
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
/-- **Alias** of `LinearIndependent.finCons`.

---

See `LinearIndependent.finCons'` for an uglier version that works if you
only have a module over a semiring.  -/
LinearIndependent.fin_cons : ∀ {K : Type u_3} {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {x : V} {n : ℕ}
  {v : Fin n → V}, LinearIndependent K v → x ∉ Submodule.span K (Set.range v) → LinearIndependent K (Fin.cons x v)
-- Mathlib.Probability.CondVar
ProbabilityTheory.condVar_of_aestronglyMeasurable : ∀ {Ω : Type u_1} {m₀ m : MeasurableSpace Ω} {hm : m ≤ m₀} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω}
  [hμm : MeasureTheory.SigmaFinite (μ.trim hm)],
  MeasureTheory.AEStronglyMeasurable X μ →
    MeasureTheory.Integrable ((X - μ[X | m]) ^ 2) μ → ProbabilityTheory.condVar m X μ =ᵐ[μ] (X - μ[X | m]) ^ 2
-- Mathlib.AlgebraicTopology.SimplicialSet.Homotopy
/-- If `H : Homotopy f g` is a homotopy between morphisms of simplicial sets
`f : X ⟶ Y` and `g : X ⟶ Y` (i.e. `H.h` is a morphism `X ⊗ Δ[1] ⟶ Y` inducing
`f` and `g`), then this is the corresponding (combinatorial) homotopy of
morphisms of simplicial objects between `f` and `g`.  -/
SSet.Homotopy.toSimplicialObjectHomotopy : {X Y : SSet} → {f g : X ⟶ Y} → SSet.Homotopy f g → CategoryTheory.SimplicialObject.Homotopy f g
-- Lean.Meta.Tactic.Grind.Main
_private.Lean.Meta.Tactic.Grind.Main.0.Lean.Meta.Grind.countersWithOriginToMessageData : String → Lean.Name → Array (Lean.Meta.Grind.Origin × Lean.Name × ℕ) → Lean.MetaM Lean.MessageData
-- Mathlib.Algebra.Order.Monoid.NatCast
ZeroLEOneClass.neZero.three : ∀ (α : Type u_1) [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [ZeroLEOneClass α] [NeZero 1] [AddLeftMono α],
  NeZero 3
-- Mathlib.CategoryTheory.Iso
CategoryTheory.IsIso.Iso.inv_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ≅ Y), CategoryTheory.inv f.hom = f.inv
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMap.ext_iff : ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H} {f g : AddConstMap G H a b},
  f = g ↔ ∀ (x : G), f x = g x
-- Init.Omega.IntList
Lean.Omega.IntList.dot_sdiv_left : ∀ (xs ys : Lean.Omega.IntList) {d : ℤ}, d ∣ ↑xs.gcd → (xs.sdiv d).dot ys = xs.dot ys / d
-- Mathlib.NumberTheory.Chebyshev
Chebyshev.theta_zero : Chebyshev.theta 0 = 0
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.below.add_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  {motive : (a a_1 : RingCat.Colimits.Prequotient F) → RingCat.Colimits.Relation F a a_1 → Prop}
  (x x' y : RingCat.Colimits.Prequotient F) (x_1 : RingCat.Colimits.Relation F x x'),
  RingCat.Colimits.Relation.below x_1 → motive x x' x_1 → RingCat.Colimits.Relation.below ⋯
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.addRightReflectLT : ∀ {α : Type u} [inst : Add α] [inst_1 : LT α] [AddRightReflectLT α], AddRightReflectLT (WithBot α)
-- Mathlib.Tactic.ITauto
/-- This is a partial application of curry.
* `ak = .and`: `(p: A ∧ B → C) (q : A) ⊢ B → C`
* `ak = .iff`: `(p: (A ↔ B) → C) (q: A → B) ⊢ (B → A) → C`
* `ak = .eq`: `(p: (A ↔ B) → C) (q: A → B) ⊢ (B → A) → C`
 -/
Mathlib.Tactic.ITauto.Proof.curry₂ : Mathlib.Tactic.ITauto.AndKind → Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.Proof
-- Mathlib.Topology.Algebra.Group.GroupTopology
AddGroupTopology.mk.inj : ∀ {α : Type u} {inst : AddGroup α} {toTopologicalSpace : TopologicalSpace α}
  {toIsTopologicalAddGroup : IsTopologicalAddGroup α} {toTopologicalSpace_1 : TopologicalSpace α}
  {toIsTopologicalAddGroup_1 : IsTopologicalAddGroup α},
  { toTopologicalSpace := toTopologicalSpace, toIsTopologicalAddGroup := toIsTopologicalAddGroup } =
      { toTopologicalSpace := toTopologicalSpace_1, toIsTopologicalAddGroup := toIsTopologicalAddGroup_1 } →
    toTopologicalSpace = toTopologicalSpace_1
-- Mathlib.LinearAlgebra.Matrix.Permanent
/-- Transposing a matrix preserves the permanent.  -/
Matrix.permanent_transpose : ∀ {n : Type u_1} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type u_2} [inst_2 : CommSemiring R]
  (M : Matrix n n R), M.transpose.permanent = M.permanent
-- Mathlib.CategoryTheory.Limits.Cones
/-- **Alias** of `CategoryTheory.Limits.Cone.cone_iso_of_hom_iso`.

---

Given a cone morphism whose object part is an isomorphism, produce an
isomorphism of cones.
 -/
CategoryTheory.Limits.Cones.cone_iso_of_hom_iso : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {K : CategoryTheory.Functor J C} {c d : CategoryTheory.Limits.Cone K} (f : c ⟶ d) [i : CategoryTheory.IsIso f.hom],
  CategoryTheory.IsIso f
-- Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
MeasureTheory.Measure.absolutelyContinuous_of_le : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α}, μ ≤ ν → μ.AbsolutelyContinuous ν
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.uIcc_prod_uIcc : ∀ {α : Type u_1} {β : Type u_2} [inst : Lattice α] [inst_1 : Lattice β] (a₁ a₂ : α) (b₁ b₂ : β),
  Set.uIcc a₁ a₂ ×ˢ Set.uIcc b₁ b₂ = Set.uIcc (a₁, b₁) (a₂, b₂)
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.insert_sdiff_singleton`. -/
Set.insert_diff_singleton : ∀ {α : Type u_1} {s : Set α} {a : α}, insert a (s \ {a}) = insert a s
-- Mathlib.Algebra.Order.Floor.Extended
ENat.toENNReal_iInf : ∀ {ι : Sort u_1} (f : ι → ℕ∞), ↑(⨅ i, f i) = ⨅ i, ↑(f i)
-- Mathlib.CategoryTheory.Filtered.Basic
/-- Any finite collection of objects in a cofiltered category has an object "to the left".
 -/
CategoryTheory.IsCofiltered.inf_objs_exists : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofiltered C] (O : Finset C),
  ∃ S, ∀ {X : C}, X ∈ O → Nonempty (S ⟶ X)
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.symm_comp_eq : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] {α : Type u_9} (e : M ≃+ N) (f : α → M) (g : α → N),
  ⇑e.symm ∘ g = f ↔ g = ⇑e ∘ f
-- Mathlib.RingTheory.Ideal.Prime
Ideal.IsPrime.mem_or_mem_of_mul_eq_zero : ∀ {α : Type u} [inst : Semiring α] {I : Ideal α}, I.IsPrime → ∀ {x y : α}, x * y = 0 → x ∈ I ∨ y ∈ I
-- Lean.Parser.Module
Lean.Parser.topLevelCommandParserFn : Lean.Parser.ParserFn
-- Mathlib.NumberTheory.ModularForms.Basic
CuspForm.hasAdd : {Γ : Subgroup (GL (Fin 2) ℝ)} → {k : ℤ} → Add (CuspForm Γ k)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_modify_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [Inhabited α]
  {k fallback : α} {f : β → β}, (t.modify k f).getKeyD k fallback = if k ∈ t then k else fallback
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremKind.default.injEq : ∀ (gen gen_1 : Bool),
  (Lean.Meta.Grind.EMatchTheoremKind.default gen = Lean.Meta.Grind.EMatchTheoremKind.default gen_1) = (gen = gen_1)
-- Mathlib.AlgebraicGeometry.Cover.Open
AlgebraicGeometry.LocallyRingedSpace.restrict.congr_simp : ∀ {U : TopCat} (X : AlgebraicGeometry.LocallyRingedSpace) {f f_1 : U ⟶ X.toTopCat} (e_f : f = f_1)
  (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)), X.restrict h = X.restrict ⋯
-- Mathlib.Data.Finset.Sups
Finset.singleton_sups_singleton : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] {a b : α}, {a} ⊻ {b} = {a ⊔ b}
-- Init.Coe
/-- Auxiliary class implementing `Coe*`.
Users should generally not implement this directly.
 -/
CoeTC : Sort u → Sort v → Sort (max (max 1 u) v)
-- Mathlib.Algebra.Field.Basic
Commute.inv_add_inv : ∀ {K : Type u_1} [inst : DivisionSemiring K] {a b : K}, Commute a b → a ≠ 0 → b ≠ 0 → a⁻¹ + b⁻¹ = (a + b) / (a * b)
-- Mathlib.Probability.Kernel.Disintegration.StandardBorel
/-- For `κ' := map κ (Prod.map (id : β → β) e)`, the hypothesis `hη` is `fst κ' ⊗ₖ η = κ'`.
With that hypothesis, `fst κ ⊗ₖ borelMarkovFromReal κ η = κ`.  -/
ProbabilityTheory.Kernel.compProd_fst_borelMarkovFromReal : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] [inst_1 : Nonempty Ω] (κ : ProbabilityTheory.Kernel α (β × Ω))
  [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel (α × β) ℝ) [ProbabilityTheory.IsSFiniteKernel η],
  (κ.map (Prod.map id (MeasureTheory.embeddingReal Ω))).fst.compProd η =
      κ.map (Prod.map id (MeasureTheory.embeddingReal Ω)) →
    κ.fst.compProd (ProbabilityTheory.Kernel.borelMarkovFromReal Ω η) = κ
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.IsStableUnderComposition.unop : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty Cᵒᵖ}
  [P.IsStableUnderComposition], P.unop.IsStableUnderComposition
-- Std.Data.DTreeMap.Internal.Balanced
Std.DTreeMap.Internal.Impl.balancedAtRoot_zero_iff' : ∀ {n : ℕ}, Std.DTreeMap.Internal.Impl.BalancedAtRoot n 0 ↔ n ≤ 1
-- Mathlib.Analysis.Complex.Circle
Circle.coe_ne_zero : ∀ (z : Circle), ↑z ≠ 0
-- Mathlib.Tactic.ClickSuggestions.Util
Mathlib.Tactic.ClickSuggestions.RwKind.hasBVars.sizeOf_spec : sizeOf Mathlib.Tactic.ClickSuggestions.RwKind.hasBVars = 1
-- Mathlib.AlgebraicTopology.DoldKan.NCompGamma
AlgebraicTopology.DoldKan.Γ₀_obj_termwise_mapMono_comp_PInfty : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (X : CategoryTheory.SimplicialObject C) {Δ Δ' : SimplexCategory} (i : Δ ⟶ Δ') [inst_2 : CategoryTheory.Mono i],
  CategoryTheory.CategoryStruct.comp
      (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono (AlgebraicTopology.AlternatingFaceMapComplex.obj X) i)
      (AlgebraicTopology.DoldKan.PInfty.f Δ.len) =
    CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f Δ'.len) (X.map i.op)
-- Mathlib.Algebra.Group.Subsemigroup.Basic
Subsemigroup.instCompleteLattice.eq_1 : ∀ {M : Type u_1} [inst : Mul M],
  Subsemigroup.instCompleteLattice =
    { le := fun x1 x2 => x1 ≤ x2, lt := fun x1 x2 => x1 < x2, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
      le_antisymm := ⋯, sup := SemilatticeSup.sup, le_sup_left := ⋯, le_sup_right := ⋯, sup_le := ⋯,
      inf := fun x1 x2 => x1 ⊓ x2, inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯,
      toSupSet := (completeLatticeOfInf (Subsemigroup M) ⋯).toSupSet, isLUB_sSup := ⋯,
      toInfSet := Subsemigroup.instInfSet, isGLB_sInf := ⋯, toTop := Subsemigroup.instTop, le_top := ⋯,
      toBot := Subsemigroup.instBot, bot_le := ⋯ }
-- Mathlib.Tactic.Translate.Reorder
Mathlib.Tactic.Translate.ArgReorder.instToMessageData : Lean.ToMessageData Mathlib.Tactic.Translate.ArgReorder
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.dblXYZ_of_Y_eq : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P Q : Fin 3 → F},
  W.Equation P →
    P 2 ≠ 0 →
      Q 2 ≠ 0 →
        P 0 * Q 2 = Q 0 * P 2 → P 1 * Q 2 = Q 1 * P 2 → P 1 * Q 2 = W.negY Q * P 2 → W.dblXYZ P = W.dblU P • ![0, 1, 0]
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
HurwitzZeta.hurwitzZetaEven_def_of_ne_or_ne : ∀ {a : UnitAddCircle} {s : ℂ},
  a ≠ 0 ∨ s ≠ 0 → HurwitzZeta.hurwitzZetaEven a s = HurwitzZeta.completedHurwitzZetaEven a s / s.Gammaℝ
-- Mathlib.Data.Seq.Computation
Computation.bind.eq_1 : ∀ {α : Type u} {β : Type v} (c : Computation α) (f : α → Computation β),
  c.bind f = Computation.corec (Computation.Bind.f f) (Sum.inl c)
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.Substring.Raw.Legacy.foldl.match_1.splitter : (motive : Substring.Raw → Sort u_1) →
  (s : Substring.Raw) →
    ((s : String) → (b e : String.Pos.Raw) → motive { str := s, startPos := b, stopPos := e }) → motive s
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
/-- Taking the product of two maps with the same codomain is equivalent to taking the product of
their domains.
See note [bundled maps over different rings] for why separate `R` and `S` semirings are used.

See `ContinuousLinearMap.coprodEquivL` for the `ContinuousLinearEquiv` version.
 -/
ContinuousLinearMap.coprodEquiv : {R : Type u_1} →
  {S : Type u_2} →
    {M : Type u_3} →
      {M₁ : Type u_5} →
        {M₂ : Type u_6} →
          [inst : Semiring R] →
            [inst_1 : TopologicalSpace M] →
              [inst_2 : TopologicalSpace M₁] →
                [inst_3 : TopologicalSpace M₂] →
                  [inst_4 : AddCommMonoid M] →
                    [inst_5 : Module R M] →
                      [inst_6 : ContinuousAdd M] →
                        [inst_7 : AddCommMonoid M₁] →
                          [inst_8 : Module R M₁] →
                            [inst_9 : AddCommMonoid M₂] →
                              [inst_10 : Module R M₂] →
                                [ContinuousAdd M₁] →
                                  [ContinuousAdd M₂] →
                                    [inst_13 : Semiring S] →
                                      [inst_14 : Module S M] →
                                        [inst_15 : ContinuousConstSMul S M] →
                                          [inst_16 : SMulCommClass R S M] →
                                            ((M₁ →L[R] M) × (M₂ →L[R] M)) ≃ₗ[S] M₁ × M₂ →L[R] M
-- Mathlib.Algebra.Central.Basic
Algebra.ofId.eq_1 : ∀ (R : Type u) (A : Type v) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  Algebra.ofId R A = { toRingHom := algebraMap R A, commutes' := ⋯ }