mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.Cotangent.map_ker_of_surjective : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {P' : Algebra.Extension R S} {f : P.Hom P'},
  Function.Surjective ⇑f →
    Ideal.comap f.toRingHom P'.ker = RingHom.ker f.toRingHom ⊔ P.ker →
      Submodule.restrictScalars P.Ring (Algebra.Extension.Cotangent.map f).ker =
        Submodule.map Algebra.Extension.Cotangent.mk
          (Submodule.comap (Submodule.subtype P.ker) (RingHom.ker f.toRingHom ⊓ P.ker))
-- Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
CategoryTheory.Sheaf.H.map_add_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_2 : CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] {F G : CategoryTheory.Sheaf J AddCommGrpCat}
  {n : ℕ} (f g : F ⟶ G) (x : F.H n),
  (CategoryTheory.Sheaf.H.map (f + g) n) x = (CategoryTheory.Sheaf.H.map f n) x + (CategoryTheory.Sheaf.H.map g n) x
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey!_eq_iff_mem_and_forall : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [inst_2 : Inhabited α],
  t ≠ ∅ → ∀ {km : α}, t.maxKey! = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.GroupTheory.Coset.Basic
Subgroup.quotientSubgroupOfMapOfLE.congr_simp : ∀ {α : Type u_1} [inst : Group α] {s t : Subgroup α} (H : Subgroup α) (h : s ≤ t) (a a_1 : ↥H ⧸ s.subgroupOf H),
  a = a_1 → Subgroup.quotientSubgroupOfMapOfLE H h a = Subgroup.quotientSubgroupOfMapOfLE H h a_1
-- Mathlib.Analysis.Quaternion
Quaternion.instInnerReal : Inner ℝ (Quaternion ℝ)
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Energy
Finpartition.energy_nonneg : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} (P : Finpartition s) (G : SimpleGraph α)
  [inst_1 : DecidableRel G.Adj], 0 ≤ P.energy G
-- Mathlib.Data.ENNReal.Inv
ENNReal.div_eq_top : ∀ {a b : ENNReal}, a / b = ⊤ ↔ a ≠ 0 ∧ b = 0 ∨ a = ⊤ ∧ b ≠ ⊤
-- Mathlib.Topology.Defs.Induced
Topology.isCoinducing_iff' : ∀ {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : X → Y),
  Topology.IsCoinducing f ↔ tY = TopologicalSpace.coinduced f tX
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.infty_coeFn_mul : ∀ {I : Type u_5} {B : I → Type u_6} [inst : (i : I) → NonUnitalNormedRing (B i)] (f g : ↥(lp B ⊤)), ↑(f * g) = ↑f * ↑g
-- Batteries.Data.PairingHeap
/-- A [pairing heap](https://en.wikipedia.org/wiki/Pairing_heap) is a data structure which supports
the following primary operations:

* `insert : α → PairingHeap α → PairingHeap α`: add an element to the heap
* `deleteMin : PairingHeap α → Option (α × PairingHeap α)`:
  remove the minimum element from the heap
* `merge : PairingHeap α → PairingHeap α → PairingHeap α`: combine two heaps

The first two operations are known as a "priority queue", so this could be called
a "mergeable priority queue". The standard choice for a priority queue is a binary heap,
which supports `insert` and `deleteMin` in `O(log n)`, but `merge` is `O(n)`.
With a `PairingHeap`, `insert` and `merge` are `O(1)`, `deleteMin` is amortized `O(log n)`.

Note that `deleteMin` may be `O(n)` in a single operation. So if you need an efficient
persistent priority queue, you should use other data structures with better worst-case time.
 -/
Batteries.PairingHeap : (α : Type u) → (α → α → Bool) → Type (max 0 u)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.ofList_cons : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {k : α}
  {v : β} {tl : List (α × β)}, Std.ExtHashMap.ofList ((k, v) :: tl) = (∅.insert k v).insertMany tl
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
/-- **Alias** of `Finset.prod_eq_mul_prod_sdiff_singleton_of_mem`. -/
Finset.prod_eq_mul_prod_diff_singleton_of_mem : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] [inst_1 : DecidableEq ι] {s : Finset ι} {i : ι},
  i ∈ s → ∀ (f : ι → M), ∏ x ∈ s, f x = f i * ∏ x ∈ s \ {i}, f x
-- Mathlib.Data.Nat.Log
Nat.log.eq_def : ∀ (b n : ℕ), Nat.log b n = if b ≤ 1 then 0 else (Nat.log.go n b n).2
-- Mathlib.Order.Filter.Map
/-- A useful lemma when dealing with uniformities.  -/
Filter.map_swap4_eq_comap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : Filter ((α × β) × γ × δ)},
  Filter.map (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) f = Filter.comap (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) f
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
/-- A monoidal category `C` is (right) monoidal closed if every object is (right) closed.  -/
CategoryTheory.MonoidalClosed : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.MonoidalCategory C] → Type (max u v)
-- Mathlib.Logic.Encodable.Basic
/-- If `α` is encodable and there is an injection `f : β → α`, then `β` is encodable as well.  -/
Encodable.ofLeftInjection : {α : Type u_1} →
  {β : Type u_2} → [Encodable α] → (f : β → α) → (finv : α → Option β) → (∀ (b : β), finv (f b) = some b) → Encodable β
-- Mathlib.Data.Set.Sups
Set.sups_subset_left : ∀ {α : Type u_2} [inst : SemilatticeSup α] {s t₁ t₂ : Set α}, t₁ ⊆ t₂ → s ⊻ t₁ ⊆ s ⊻ t₂
-- Mathlib.Data.Fin.Tuple.Sort
/-- A permutation `σ` equals `sort f` if and only if `f ∘ σ` is monotone and whenever `i < j`
and `f (σ i) = f (σ j)`, then `σ i < σ j`. This means that `sort f` is the lexicographically
smallest permutation `σ` such that `f ∘ σ` is monotone.  -/
Tuple.eq_sort_iff : ∀ {n : ℕ} {α : Type u_1} [inst : LinearOrder α] {f : Fin n → α} {σ : Equiv.Perm (Fin n)},
  σ = Tuple.sort f ↔ Monotone (f ∘ ⇑σ) ∧ ∀ (i j : Fin n), i < j → f (σ i) = f (σ j) → σ i < σ j
-- Mathlib.Topology.Homeomorph.Defs
Equiv.toHomeomorphOfContinuousOpen_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : X ≃ Y)
  (h₁ : Continuous ⇑e) (h₂ : IsOpenMap ⇑e), ⇑(e.toHomeomorphOfContinuousOpen h₁ h₂) = ⇑e
-- Std.Do.PostCond
/-- An assertion about the possible exceptions in `ps` that always holds.
 -/
Std.Do.ExceptConds.true : {ps : Std.Do.PostShape} → Std.Do.ExceptConds ps
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.SimprocOLeanEntry.mk.inj : ∀ {declName : Lean.Name} {post : Bool} {keys : Array Lean.Meta.SimpTheoremKey} {declName_1 : Lean.Name} {post_1 : Bool}
  {keys_1 : Array Lean.Meta.SimpTheoremKey},
  { declName := declName, post := post, keys := keys } = { declName := declName_1, post := post_1, keys := keys_1 } →
    declName = declName_1 ∧ post = post_1 ∧ keys = keys_1
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.Ext.biprodAddEquiv_apply_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X₁ X₂ Y : C} {n : ℕ} (e : CategoryTheory.Abelian.Ext (X₁ ⊞ X₂) Y n),
  (CategoryTheory.Abelian.Ext.biprodAddEquiv e).1 =
    (CategoryTheory.Abelian.Ext.mk₀ CategoryTheory.Limits.biprod.inl).comp e ⋯
-- Mathlib.Algebra.MvPolynomial.CommRing
MvPolynomial.degreeOf_neg : ∀ {R : Type u} {σ : Type u_1} [inst : CommRing R] (i : σ) (p : MvPolynomial σ R),
  MvPolynomial.degreeOf i (-p) = MvPolynomial.degreeOf i p
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.eventually_r_lt_n : ∀ {α : Type u_1} [inst : Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [inst_1 : Nonempty α]
  (R : AkraBazziRecurrence T g a b r), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : α), r i n < n
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instMonoidWithZero : {M₀ : Type u_1} →
  [inst : TopologicalSpace M₀] →
    [inst_1 : MonoidWithZero M₀] → [ContinuousMul M₀] → MonoidWithZero (SeparationQuotient M₀)
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.divConst_empty_left : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] (B : Finset G), ∅.divConst B = 0
-- Lean.DocString.Syntax
Lean.Doc.Syntax.metadataContents.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.ForwardSliceSearcher.buildTable.eq_1 : ∀ (pat : String.Slice),
  String.Slice.Pattern.ForwardSliceSearcher.buildTable pat =
    if h : pat.utf8ByteSize = 0 then Vector.cast ⋯ #v[]
    else
      let arr := Array.emptyWithCapacity pat.utf8ByteSize;
      let arr' := arr.push 0;
      String.Slice.Pattern.ForwardSliceSearcher.buildTable.go✝ pat arr' ⋯ ⋯ ⋯
-- Mathlib.RingTheory.Flat.Basic
Module.Flat.shrink : ∀ {R : Type u} {M : Type v} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Small.{v', v} M] [Module.Flat R M], Module.Flat R (Shrink.{v', v} M)
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.denom_cocycle' : ∀ (g h : GL (Fin 2) ℝ) (z : UpperHalfPlane),
  UpperHalfPlane.denom (g * h) ↑z =
    (UpperHalfPlane.σ h) (UpperHalfPlane.denom g ↑(UpperHalfPlane.smulAux h z)) * UpperHalfPlane.denom h ↑z
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pullback_map_diagonal_isPullback : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C]
  {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [inst_2 : CategoryTheory.Limits.HasPullback i i]
  [inst_3 : CategoryTheory.Limits.HasPullback f g]
  [inst_4 :
    CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)]
  [CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.diagonal i)
      (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i)
        (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)],
  CategoryTheory.IsPullback (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) f)
    (CategoryTheory.Limits.pullback.map f g (CategoryTheory.CategoryStruct.comp f i)
      (CategoryTheory.CategoryStruct.comp g i) (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id Y)
      i ⋯ ⋯)
    (CategoryTheory.Limits.pullback.diagonal i)
    (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i)
      (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
/-- Lower bound on the edge densities between parts of `SzemerediRegularity.increment`. This is the
blanket lower bound used the uniform parts.  -/
SzemerediRegularity.edgeDensity_chunk_uniform : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {P : Finpartition Finset.univ} {hP : P.IsEquipartition}
  {G : SimpleGraph α} [inst_2 : DecidableRel G.Adj] {ε : ℝ} {U V : Finset α} [Nonempty α],
  P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α →
    100 ≤ 4 ^ P.parts.card * ε ^ 5 →
      ∀ (hU : U ∈ P.parts) (hV : V ∈ P.parts),
        ↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 ≤
          (∑ ab ∈ (SzemerediRegularity.chunk hP G ε hU).parts.product (SzemerediRegularity.chunk hP G ε hV).parts,
              ↑(G.edgeDensity ab.1 ab.2) ^ 2) /
            16 ^ P.parts.card
-- Lean.Meta.Sym.Simp.SimpM
Lean.Meta.Sym.Simp.Config.mk.injEq : ∀ (maxSteps maxDischargeDepth maxSteps_1 maxDischargeDepth_1 : ℕ),
  ({ maxSteps := maxSteps, maxDischargeDepth := maxDischargeDepth } =
      { maxSteps := maxSteps_1, maxDischargeDepth := maxDischargeDepth_1 }) =
    (maxSteps = maxSteps_1 ∧ maxDischargeDepth = maxDischargeDepth_1)
-- Mathlib.AlgebraicTopology.SimplexCategory.Truncated
SimplexCategory.Truncated.δ₂_two_comp_σ₂_one_assoc : ∀ {Z : CategoryTheory.ObjectProperty.FullSubcategory fun a => a.len ≤ 2}
  (h : { obj := { len := 1 }, property := SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_1 } ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (SimplexCategory.Truncated.δ₂ 2 SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_1
        SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_2)
      (CategoryTheory.CategoryStruct.comp
        (SimplexCategory.Truncated.σ₂ 1 SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_2
          SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_1)
        h) =
    h
-- Mathlib.LinearAlgebra.Dimension.Basic
rank_le_card : ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Module.rank R M ≤ Cardinal.mk M
-- Mathlib.Data.Set.Finite.Basic
Set.fintypeTop : {α : Type u} → [Fintype α] → Fintype ↑⊤
-- Lean.Meta.Tactic.Grind.Arith.Linear.Reify
Lean.Meta.Grind.Arith.Linear.isSMulNatInst : Lean.Meta.Grind.Arith.Linear.Struct → Lean.Expr → Bool
-- Mathlib.Order.Filter.Extr
IsMinFilter.tendsto_principal_Ici : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
  IsMinFilter f l a → Filter.Tendsto f l (Filter.principal (Set.Ici (f a)))
-- Mathlib.RingTheory.HopkinsLevitzki
isArtinianRing_iff_isNilpotent_maximalIdeal : ∀ (R : Type u_3) [inst : CommRing R] [IsNoetherianRing R] [inst_2 : IsLocalRing R],
  IsArtinianRing R ↔ IsNilpotent (IsLocalRing.maximalIdeal R)
-- Mathlib.Data.FP.Basic
Int.shift2 : ℕ → ℕ → ℤ → ℕ × ℕ
-- Mathlib.Tactic.TermCongr
/-- Ensures the expected type is a HEq. Returns the HEq.
This expression satisfies `Lean.Expr.heq?`.  -/
Mathlib.Tactic.TermCongr.mkHEqForExpectedType : Option Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapGrp.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal],
  F.mapGrp =
    { obj := fun A => { X := F.obj A.X, grp := CategoryTheory.Functor.grpObjObj },
      map := fun {X Y} f => CategoryTheory.Grp.homMk' (F.mapMon.map f.hom), map_id := ⋯, map_comp := ⋯ }
-- Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Subalgebra.unop_sSup : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (S : Set (Subalgebra R Aᵐᵒᵖ)), (sSup S).unop = sSup (Subalgebra.op ⁻¹' S)
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_castSuccEmb_Iic : ∀ {n : ℕ} (i : Fin n), Finset.map Fin.castSuccEmb (Finset.Iic i) = Finset.Iic i.castSucc
-- Mathlib.Data.Nat.DvdSequence
/-- A function `f : α → β` is a divisibility sequence if `a ∣ b` implies `f a ∣ f b`.  -/
IsDvdSequence : {α : Type u_1} → {β : Type u_2} → [Dvd α] → [Dvd β] → (α → β) → Prop
-- Mathlib.Analysis.SpecificLimits.Normed
summable_choose_mul_geometric_of_norm_lt_one : ∀ {R : Type u_4} [inst : NormedRing R] [HasSummableGeomSeries R] (k : ℕ) {r : R},
  ‖r‖ < 1 → Summable fun n => ↑((n + k).choose k) * r ^ n
-- Init.Data.Vector.Lemmas
Vector.contains_iff_mem : ∀ {α : Type u_1} {n : ℕ} [inst : BEq α] [LawfulBEq α] {a : α} {as : Vector α n}, as.contains a = true ↔ a ∈ as
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.LHom.onTerm.eq_def : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} (φ : L →ᴸ L') (x : L.Term α),
  φ.onTerm x =
    match x with
    | FirstOrder.Language.var i => FirstOrder.Language.var i
    | FirstOrder.Language.func f ts => FirstOrder.Language.func (φ.onFunction f) fun i => φ.onTerm (ts i)
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.type_prod_lex : ∀ {α β : Type u} (r : α → α → Prop) (s : β → β → Prop) [inst : IsWellOrder α r] [inst_1 : IsWellOrder β s],
  Ordinal.type (Prod.Lex s r) = Ordinal.type r * Ordinal.type s
-- Init.Data.String.Basic
String.push_induction : ∀ (s : String) (motive : String → Prop),
  motive "" → (∀ (b : String) (c : Char), motive b → motive (b.push c)) → motive s
-- Mathlib.Order.Filter.Map
Filter.filter_injOn_Iic_iff_injOn : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {m : α → β},
  Set.InjOn (Filter.map m) (Set.Iic (Filter.principal s)) ↔ Set.InjOn m s
-- Mathlib.Order.Interval.Set.Basic
Set.decidableMemIic : {α : Type u_1} → [inst : Preorder α] → {b x : α} → [Decidable (x ≤ b)] → Decidable (x ∈ Set.Iic b)
-- Mathlib.Analysis.Complex.UpperHalfPlane.Metric
/-- For two points on the same vertical line, the distance is equal to the distance between the
logarithms of their imaginary parts.  -/
UpperHalfPlane.dist_of_re_eq : ∀ {z w : UpperHalfPlane}, z.re = w.re → dist z w = dist (Real.log z.im) (Real.log w.im)
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Bicategory.Adjunction.mk : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} →
      {f : a ⟶ b} →
        {g : b ⟶ a} →
          (unit : CategoryTheory.CategoryStruct.id a ⟶ CategoryTheory.CategoryStruct.comp f g) →
            (counit : CategoryTheory.CategoryStruct.comp g f ⟶ CategoryTheory.CategoryStruct.id b) →
              autoParam
                  (CategoryTheory.Bicategory.leftZigzag unit counit =
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor f).hom
                      (CategoryTheory.Bicategory.rightUnitor f).inv)
                  CategoryTheory.Bicategory.Adjunction.left_triangle._autoParam →
                autoParam
                    (CategoryTheory.Bicategory.rightZigzag unit counit =
                      CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor g).hom
                        (CategoryTheory.Bicategory.leftUnitor g).inv)
                    CategoryTheory.Bicategory.Adjunction.right_triangle._autoParam →
                  CategoryTheory.Bicategory.Adjunction f g
-- Init.Data.BitVec.Lemmas
BitVec.toNat_not : ∀ {v : ℕ} {x : BitVec v}, (~~~x).toNat = 2 ^ v - 1 - x.toNat
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
/-- The canonical isomorphism between the localization of a quotient module and its realization
as a quotient of the localized module.  -/
localizedQuotientEquiv : {R : Type u_5} →
  {M : Type u_7} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          (p : Submonoid R) →
            (M' : Submodule R M) →
              (LocalizedModule p M ⧸ Submodule.localized p M') ≃ₗ[Localization p] LocalizedModule p (M ⧸ M')
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.triangleLEGE_map_hom₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b) {X Y : C} (φ : X ⟶ Y),
  ((t.triangleLEGE a b h).map φ).hom₁ = (t.truncLE a).map φ
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.all₂.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : List α → List β → Sort u_3) →
      (x : List α) →
        (x_1 : List β) →
          (Unit → motive [] []) →
            ((a : α) → (as : List α) → (b : β) → (bs : List β) → motive (a :: as) (b :: bs)) →
              ((x : List α) →
                  (x_2 : List β) →
                    (x = [] → x_2 = [] → False) →
                      (∀ (a : α) (as : List α) (b : β) (bs : List β), x = a :: as → x_2 = b :: bs → False) →
                        motive x x_2) →
                motive x x_1
-- Init.Data.List.Int.Sum
List.sum_le_max_mul_length_of_max?_eq_some_int : ∀ {x : ℤ} {xs : List ℤ}, xs.max? = some x → xs.sum ≤ x * ↑xs.length
-- Mathlib.CategoryTheory.Functor.Derived.LeftDerived
/-- The natural transformation `LF' ⟶ LF` on left derived functors that is
induced by a natural transformation `F' ⟶ F`.  -/
CategoryTheory.Functor.leftDerivedNatTrans : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_5, u_3} H] →
            (LF' LF : CategoryTheory.Functor D H) →
              {F F' : CategoryTheory.Functor C H} →
                {L : CategoryTheory.Functor C D} →
                  (L.comp LF' ⟶ F') →
                    (α : L.comp LF ⟶ F) →
                      (W : CategoryTheory.MorphismProperty C) →
                        [inst_3 : L.IsLocalization W] → [LF.IsLeftDerivedFunctor α W] → (F' ⟶ F) → (LF' ⟶ LF)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_ideal : ∀ {X : AlgebraicGeometry.Scheme} (Z : TopologicalSpace.Closeds ↥X) (U : ↑X.affineOpens),
  (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal Z).ideal U =
    PrimeSpectrum.vanishingIdeal (⇑(AlgebraicGeometry.IsAffineOpen.fromSpec ⋯) ⁻¹' ↑Z)
-- Mathlib.Order.DirSupClosed
DirSupClosed.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] (s : Set α),
  DirSupClosed s =
    ∀ ⦃d : Set α⦄, d ⊆ s → d.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- A morphism of `0`-hypercovers is a morphism of the underlying pre-`0`-hypercovers.  -/
CategoryTheory.Precoverage.ZeroHypercover.Hom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.Precoverage C) → {S : C} → J.ZeroHypercover S → J.ZeroHypercover S → Type (max (max v w) w')
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Set.powersetCard.permOfDisjoint.eq_1 : ∀ {m n : ℕ} {I : Type u_2} [inst : LinearOrder I] {s : ↑(Set.powersetCard I m)} {t : ↑(Set.powersetCard I n)}
  (h : Disjoint ↑s ↑t),
  Set.powersetCard.permOfDisjoint h =
    finSumFinEquiv.symm.trans
      ((↑((Set.powersetCard.orderIsoOfFin s).sumCongr (Set.powersetCard.orderIsoOfFin t))).trans
        ((Equiv.Finset.disjUnionEquiv (↑s) (↑t) h).trans
          ↑(Set.powersetCard.orderIsoOfFin (Set.powersetCard.disjUnion h)).symm))
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char
Char.reduceIsDigit : Lean.Meta.Simp.DSimproc
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.instCoeContMDiffMap : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                {H : Type u_5} →
                  [inst_5 : TopologicalSpace H] →
                    {H' : Type u_6} →
                      [inst_6 : TopologicalSpace H'] →
                        {I : ModelWithCorners 𝕜 E H} →
                          {I' : ModelWithCorners 𝕜 E' H'} →
                            {M : Type u_9} →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace H M] →
                                  {M' : Type u_10} →
                                    [inst_9 : TopologicalSpace M'] →
                                      [inst_10 : ChartedSpace H' M'] →
                                        {n : WithTop ℕ∞} → Coe (Diffeomorph I I' M M' n) (ContMDiffMap I I' M M' n)
-- Init.PropLemmas
/-- `∨` distributes over `∧` (on the left).  -/
or_and_left : ∀ {a b c : Prop}, a ∨ b ∧ c ↔ (a ∨ b) ∧ (a ∨ c)
-- Mathlib.Topology.Instances.Discrete
discreteTopology_iff_orderTopology_of_pred_succ : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [PredOrder α] [SuccOrder α],
  DiscreteTopology α ↔ OrderTopology α
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.ForwardPattern.mk : {ρ : Type} →
  {pat : ρ} →
    ((s : String.Slice) → Option s.Pos) →
      ((s : String.Slice) → s.isEmpty = false → Option s.Pos) →
        (String.Slice → Bool) → String.Slice.Pattern.ForwardPattern pat
-- Mathlib.Computability.EpsilonNFA
εNFA.εClosure.below : {α : Type u} →
  {σ : Type v} →
    {M : εNFA α σ} → {S : Set σ} → {motive : (a : σ) → M.εClosure S a → Prop} → {a : σ} → M.εClosure S a → Prop
-- Mathlib.Algebra.CubicDiscriminant
Cubic.equiv_symm_apply_d : ∀ {R : Type u_1} [inst : Semiring R] (f : { p // p.degree ≤ 3 }), (Cubic.equiv.symm f).d = (↑f).coeff 0