mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂.comp.injEq : ∀ (e : Lean.Expr) (isoLift? : Option Mathlib.Tactic.BicategoryLike.IsoLift) (f g h : Mathlib.Tactic.BicategoryLike.Mor₁)
  (η θ : Mathlib.Tactic.BicategoryLike.Mor₂) (e_1 : Lean.Expr)
  (isoLift?_1 : Option Mathlib.Tactic.BicategoryLike.IsoLift) (f_1 g_1 h_1 : Mathlib.Tactic.BicategoryLike.Mor₁)
  (η_1 θ_1 : Mathlib.Tactic.BicategoryLike.Mor₂),
  (Mathlib.Tactic.BicategoryLike.Mor₂.comp e isoLift? f g h η θ =
      Mathlib.Tactic.BicategoryLike.Mor₂.comp e_1 isoLift?_1 f_1 g_1 h_1 η_1 θ_1) =
    (e = e_1 ∧ isoLift? = isoLift?_1 ∧ f = f_1 ∧ g = g_1 ∧ h = h_1 ∧ η = η_1 ∧ θ = θ_1)
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.smulCommClass : ∀ {R : Type u} [inst : Semiring R] {S₁ : Type u_1} {S₂ : Type u_2} [inst_1 : SMulZeroClass S₁ R]
  [inst_2 : SMulZeroClass S₂ R] [SMulCommClass S₁ S₂ R], SMulCommClass S₁ S₂ (Polynomial R)
-- Mathlib.Analysis.Complex.PhragmenLindelof
/-- **Phragmen-Lindelöf principle** in a strip `U = {z : ℂ | a < re z < b}`.
Let `f g : ℂ → E` be functions such that

* `f` and `g` are differentiable on `U` and are continuous on its closure;
* `‖f z‖` and `‖g z‖` are bounded from above by `A * exp(B * exp(c * |im z|))` on `U` for some
  `c < π / (b - a)`;
* `f z = g z` on the boundary of `U`.

Then `f` is equal to `g` on the closed strip `{z : ℂ | a ≤ re z ≤ b}`.
 -/
PhragmenLindelof.eqOn_vertical_strip : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {a b : ℝ} {f g : ℂ → E},
  DiffContOnCl ℂ f (Complex.re ⁻¹' Set.Ioo a b) →
    (∃ c < Real.pi / (b - a),
        ∃ B,
          f =O[Filter.comap (abs ∘ Complex.im) Filter.atTop ⊓ Filter.principal (Complex.re ⁻¹' Set.Ioo a b)] fun z =>
            Real.exp (B * Real.exp (c * |z.im|))) →
      DiffContOnCl ℂ g (Complex.re ⁻¹' Set.Ioo a b) →
        (∃ c < Real.pi / (b - a),
            ∃ B,
              g =O[Filter.comap (abs ∘ Complex.im) Filter.atTop ⊓ Filter.principal (Complex.re ⁻¹' Set.Ioo a b)]
                fun z => Real.exp (B * Real.exp (c * |z.im|))) →
          (∀ (z : ℂ), z.re = a → f z = g z) →
            (∀ (z : ℂ), z.re = b → f z = g z) → Set.EqOn f g (Complex.re ⁻¹' Set.Icc a b)
-- Mathlib.Combinatorics.SetFamily.Intersecting
Set.intersecting_empty : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α], ∅.Intersecting
-- Mathlib.CategoryTheory.Core
CategoryTheory.Functor.coreId_hom_app_iso_hom : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (X : CategoryTheory.Core C),
  ((CategoryTheory.Functor.coreId C).hom.app X).iso.hom = CategoryTheory.CategoryStruct.id X.of
-- Mathlib.Data.EReal.Basic
EReal.instCoeReal : Coe ℝ EReal
-- Init.Data.Vector.Lemmas
Vector.all_mk : ∀ {α : Type u_1} {n : ℕ} {p : α → Bool} {xs : Array α} (h : xs.size = n), (Vector.mk xs h).all p = xs.all p
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.comp_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} {n : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n),
  z₁.comp (CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.id G)) ⋯ = z₁
-- Mathlib.LinearAlgebra.BilinearMap
/-- A version of `Function.Surjective.comp` for composition of a bilinear map with a linear map.  -/
LinearMap.surjective_compr₂_of_exists_rightInverse : ∀ {R : Type u_2} [inst : CommSemiring R] {M : Type u_5} {Nₗ : Type u_8} {Pₗ : Type u_9} {Qₗ : Type u_10}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid Nₗ] [inst_3 : AddCommMonoid Pₗ] [inst_4 : AddCommMonoid Qₗ]
  [inst_5 : Module R M] [inst_6 : Module R Nₗ] [inst_7 : Module R Pₗ] [inst_8 : Module R Qₗ] (f : M →ₗ[R] Nₗ →ₗ[R] Pₗ)
  (g : Pₗ →ₗ[R] Qₗ), Function.Surjective ⇑f → (∃ g', g ∘ₗ g' = LinearMap.id) → Function.Surjective ⇑(f.compr₂ g)
-- Mathlib.Data.Int.Log
Int.log_ofNat : ∀ {R : Type u_1} [inst : Semifield R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorSemiring R]
  (b n : ℕ) [inst_4 : n.AtLeastTwo], Int.log b (OfNat.ofNat n) = ↑(Nat.log b (OfNat.ofNat n))
-- Mathlib.Tactic.Module
Mathlib.Tactic.Module.NF.eval.eq_1 : ∀ {R : Type u_2} {M : Type u_3} [inst : Add M] [inst_1 : Zero M] [inst_2 : SMul R M] (l : Mathlib.Tactic.Module.NF R M),
  l.eval =
    (List.map
        (fun x =>
          match x with
          | (r, x) => r • x)
        l).sum
-- Mathlib.NumberTheory.Divisors
_private.Mathlib.NumberTheory.Divisors.0.Int.termNatCast : Lean.ParserDescr
-- Mathlib.Topology.Order.PartialSups
ContinuousWithinAt.partialSups_apply : ∀ {L : Type u_1} [inst : SemilatticeSup L] [inst_1 : TopologicalSpace L] [ContinuousSup L] {X : Type u_2}
  [inst_3 : TopologicalSpace X] {f : ℕ → X → L} {n : ℕ} {s : Set X} {x : X},
  (∀ k ≤ n, ContinuousWithinAt (f k) s x) → ContinuousWithinAt (fun a => (partialSups fun x => f x a) n) s x
-- Mathlib.Topology.Compactness.Lindelof
IsLindelof.insert : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsLindelof s → ∀ (a : X), IsLindelof (insert a s)
-- Init.Data.Iterators.Lemmas.Consumers.Collect
Std.Iter.toList_toArray_ensureTermination : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [inst_1 : Std.Iterators.Finite α Id] {it : Std.Iter β},
  it.ensureTermination.toArray.toList = it.toList
-- Mathlib.Algebra.Free
FreeAddMagma.add_seq : ∀ {α β : Type u} {f g : FreeAddMagma (α → β)} {x : FreeAddMagma α}, f + g <*> x = (f <*> x) + (g <*> x)
-- Mathlib.Algebra.Order.Ring.Idempotent
/-- In a commutative ring, the idempotents are in 1-1 correspondence with pairs of elements
whose product is 0 and whose sum is 1. The correspondence is given by `a ↔ (a, 1 - a)`.  -/
OrderIso.isIdempotentElemMulZeroAddOne : {R : Type u_1} → [inst : CommRing R] → { a // IsIdempotentElem a } ≃o { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.IsTheta.comp_fst : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F}
  {l : Filter α} (l' : Filter β), f =Θ[l] g → (f ∘ Prod.fst) =Θ[l ×ˢ l'] (g ∘ Prod.fst)
-- Mathlib.Order.Filter.AtTopBot.Basic
/-- A function `f` maps downwards closed sets (atBot sets) to downwards closed sets when it is a
Galois coinsertion. The Galois "coinsertion" and "connection" is weakened to only require it to be
an insertion and a connection below `b`.  -/
Filter.map_atBot_eq_of_gc : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [IsCodirectedOrder α] [inst_2 : PartialOrder β]
  [IsCodirectedOrder β] {f : α → β} (g : β → α) (b : β),
  Monotone f →
    (∀ (a : α), ∀ c ≤ b, c ≤ f a ↔ g c ≤ a) → (∀ c ≤ b, f (g c) ≤ c) → Filter.map f Filter.atBot = Filter.atBot
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.IsHomogeneous.add : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {f g : MvPowerSeries σ R} {p : ℕ},
  f.IsHomogeneous p → g.IsHomogeneous p → (f + g).IsHomogeneous p
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
SSet.Truncated.Path₁.mk : {X : SSet.Truncated 1} →
  {n : ℕ} →
    (vertex : Fin (n + 1) → X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Path₁._proof_1 })) →
      (arrow : Fin n → X.obj (Opposite.op { obj := { len := 1 }, property := SSet.Truncated.Path₁._proof_2 })) →
        (∀ (i : Fin n),
            (CategoryTheory.ConcreteCategory.hom
                  (X.map
                    (SimplexCategory.Truncated.Hom.tr (SimplexCategory.δ 1) SSet.Truncated.Path₁._proof_1
                        SSet.Truncated.Path₁._proof_5).op))
                (arrow i) =
              vertex i.castSucc) →
          (∀ (i : Fin n),
              (CategoryTheory.ConcreteCategory.hom
                    (X.map
                      (SimplexCategory.Truncated.Hom.tr (SimplexCategory.δ 0) SSet.Truncated.Path₁._proof_1
                          SSet.Truncated.Path₁._proof_5).op))
                  (arrow i) =
                vertex i.succ) →
            X.Path₁ n
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
List.aestronglyMeasurable_prod : ∀ {α : Type u_1} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {M : Type u_5} [inst : Monoid M]
  [inst_1 : TopologicalSpace M] [ContinuousMul M] (l : List (α → M)),
  (∀ f ∈ l, MeasureTheory.AEStronglyMeasurable f μ) → MeasureTheory.AEStronglyMeasurable l.prod μ
-- Mathlib.Algebra.Order.ToIntervalMod
QuotientAddGroup.btw_coe_iff' : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} [hp' : Fact (0 < p)] {x₁ x₂ x₃ : α}, btw ↑x₁ ↑x₂ ↑x₃ ↔ toIcoMod ⋯ 0 (x₂ - x₁) ≤ toIocMod ⋯ 0 (x₃ - x₁)
-- Mathlib.Order.Filter.Basic
Filter.EventuallyEq.sub_eq : ∀ {α : Type u} {β : Type v} [inst : AddGroup β] {f g : α → β} {l : Filter α}, f =ᶠ[l] g → f - g =ᶠ[l] 0
-- Mathlib.Data.Finset.Insert
Finset.insert_nonempty : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Finset α), (insert a s).Nonempty
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.preimage_iSup : ∀ {X Y : SSet} {ι : Type u_1} (A : ι → X.Subcomplex) (p : Y ⟶ X), (⨆ i, A i).preimage p = ⨆ i, (A i).preimage p
-- Mathlib.NumberTheory.Padics.PadicNorm
padicNorm.dvd_iff_norm_le : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} {z : ℤ}, ↑(p ^ n) ∣ z ↔ padicNorm p ↑z ≤ ↑p ^ (-↑n)
-- Mathlib.RingTheory.Frobenius
MulSemiringAction.toAlgHom.congr_simp : ∀ {M : Type u_1} (R : Type u_3) (A : Type u_4) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Monoid M] [inst_4 : MulSemiringAction M A] [inst_5 : SMulCommClass M R A] (m m_1 : M),
  m = m_1 → MulSemiringAction.toAlgHom R A m = MulSemiringAction.toAlgHom R A m_1
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get!_diff_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [inst : Inhabited α] [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₁ → (t₁ \ t₂).get! k = default
-- Mathlib.Computability.Language
Language.iSup_sub : ∀ {α : Type u_1} {ι : Sort v} (l : ι → Language α) (m : Language α), (⨆ i, l i) - m = ⨆ i, l i - m
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.w_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor J C) [inst_2 : CategoryTheory.Limits.HasColimit F] {j j' : J} (f : j' ⟶ j) {Z : C}
  (h : CategoryTheory.Limits.colimit F ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j') h
-- Mathlib.Order.GaloisConnection.Defs
/-- **Alias** of `GaloisCoinsertion.leftInverse_u_l`. -/
GaloisCoinsertion.u_l_leftInverse : ∀ {α : Type u} {β : Type v} {u : α → β} {l : β → α} [inst : Preorder α] [inst_1 : PartialOrder β]
  (gi : GaloisCoinsertion l u), Function.LeftInverse u l
-- Init.Prelude
/-- `a ^ n` computes `a` to the power of `n` where `n : Nat`. See `Pow`.  -/
NatPow.pow : {α : Type u} → [self : NatPow α] → α → ℕ → α
-- Mathlib.AlgebraicTopology.SimplicialSet.Nerve
CategoryTheory.nerve.homEquiv_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {x y : CategoryTheory.ComposableArrows C 0}
  (e : SSet.Edge x y),
  CategoryTheory.nerve.homEquiv e =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.hom e.edge) (CategoryTheory.eqToHom ⋯))
-- Mathlib.Algebra.Order.Group.Defs
inv_le_self_iff : ∀ {α : Type u} [inst : CommGroup α] [inst_1 : LinearOrder α] [IsOrderedMonoid α] {a : α}, a⁻¹ ≤ a ↔ 1 ≤ a
-- Mathlib.Topology.EMetricSpace.Defs
/-- Pseudoemetric space instance on the multiplicative opposite of a pseudoemetric space.  -/
MulOpposite.instPseudoEMetricSpace : {α : Type u_2} → [PseudoEMetricSpace α] → PseudoEMetricSpace αᵐᵒᵖ
-- Mathlib.GroupTheory.Perm.List
List.formPerm_apply_lt_getElem : ∀ {α : Type u_1} [inst : DecidableEq α] (xs : List α),
  xs.Nodup → ∀ (n : ℕ) (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
-- Mathlib.LinearAlgebra.Projectivization.Constructions
Projectivization.cross_mk : ∀ {F : Type u_1} [inst : Field F] [inst_1 : DecidableEq F] {v w : Fin 3 → F} (hv : v ≠ 0) (hw : w ≠ 0),
  (Projectivization.mk F v hv).cross (Projectivization.mk F w hw) =
    if h : (crossProduct v) w = 0 then Projectivization.mk F v hv else Projectivization.mk F ((crossProduct v) w) h
-- Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
sInf_div : ∀ {M : Type u_1} [inst : CompleteLattice M] [inst_1 : Group M] [MulLeftMono M] [MulRightMono M] (s t : Set M),
  sInf (s / t) = sInf s / sSup t
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int16.reduceToInt : Lean.Meta.Simp.DSimproc
-- Mathlib.CategoryTheory.Localization.Triangulated
CategoryTheory.MorphismProperty.IsCompatibleWithTriangulation.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Limits.HasZeroObject C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {W : CategoryTheory.MorphismProperty C} [toIsCompatibleWithShift : W.IsCompatibleWithShift ℤ],
  (∀ (T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C),
      T₁ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
        T₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
          ∀ (a : T₁.obj₁ ⟶ T₂.obj₁) (b : T₁.obj₂ ⟶ T₂.obj₂),
            W a →
              W b →
                CategoryTheory.CategoryStruct.comp T₁.mor₁ b = CategoryTheory.CategoryStruct.comp a T₂.mor₁ →
                  ∃ c,
                    ∃ (_ : W c),
                      CategoryTheory.CategoryStruct.comp T₁.mor₂ c = CategoryTheory.CategoryStruct.comp b T₂.mor₂ ∧
                        CategoryTheory.CategoryStruct.comp T₁.mor₃ ((CategoryTheory.shiftFunctor C 1).map a) =
                          CategoryTheory.CategoryStruct.comp c T₂.mor₃) →
    W.IsCompatibleWithTriangulation
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.foldl_eq_foldl_keysArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {δ : Type w} {f : δ → α → δ} {init : δ},
  Std.TreeMap.foldl (fun d a x => f d a) init t = Array.foldl f init t.keysArray
-- Mathlib.RingTheory.WittVector.WittPolynomial
xInTermsOfW.eq_def : ∀ (p : ℕ) (R : Type u_1) [inst : CommRing R] [inst_1 : Invertible ↑p] (x : ℕ),
  xInTermsOfW p R x =
    have n := x;
    (MvPolynomial.X n - ∑ i, MvPolynomial.C (↑p ^ ↑i) * xInTermsOfW p R ↑i ^ p ^ (n - ↑i)) * MvPolynomial.C (⅟↑p ^ n)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKeyD_modify_eq_maxKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  {k : α} {f : β → β} {fallback : α}, (t.modify k f).maxKeyD fallback = t.maxKeyD fallback
-- Mathlib.Analysis.Analytic.Constructions
/-- Finproducts of analytic functions are analytic  -/
analyticAt_finprod : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {α : Type u_9} {A : Type u_10} [inst_3 : NormedCommRing A] [inst_4 : NormedAlgebra 𝕜 A]
  {f : α → E → A} {c : E}, (∀ (a : α), AnalyticAt 𝕜 (f a) c) → AnalyticAt 𝕜 (∏ᶠ (n : α), f n) c
-- Mathlib.Data.Fin.SuccPred
Fin.exists_succ_eq : ∀ {n : ℕ} {x : Fin (n + 1)}, (∃ y, y.succ = x) ↔ x ≠ 0
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
ProfiniteAddGrp.ProfiniteCompletion.preimage_le : ∀ {G : AddGrpCat} {P : ProfiniteAddGrp.{u}} {f : G ⟶ AddGrpCat.of ↑P.toProfinite.toTop}
  {H K : OpenNormalAddSubgroup ↑P.toProfinite.toTop},
  H ≤ K → ProfiniteAddGrp.ProfiniteCompletion.preimage f H ≤ ProfiniteAddGrp.ProfiniteCompletion.preimage f K
-- Mathlib.Data.PFunctor.Univariate.M
/-- destructor for M-types, similar to `casesOn` but also
gives access directly to the root and subtrees on an M-type  -/
PFunctor.M.casesOn' : {F : PFunctor.{uA, uB}} →
  {r : F.M → Sort w} → (x : F.M) → ((a : F.A) → (f : F.B a → F.M) → r (PFunctor.M.mk ⟨a, f⟩)) → r x
-- Mathlib.GroupTheory.Perm.Basic
Set.BijOn.perm_pow : ∀ {α : Type u_1} {f : Equiv.Perm α} {s : Set α}, Set.BijOn (⇑f) s s → ∀ (n : ℕ), Set.BijOn (⇑(f ^ n)) s s
-- Aesop.Script.TacticState
Aesop.Script.TacticState : Type
-- Mathlib.Analysis.Normed.Group.Bounded
HasCompactMulSupport.exists_pos_le_norm : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddGroup α] {f : α → E} [inst_1 : One E],
  HasCompactMulSupport f → ∃ R, 0 < R ∧ ∀ (x : α), R ≤ ‖x‖ → f x = 1
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.mopMopEquivalenceInverseMonoidal_η_unmop_unmop : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  (CategoryTheory.Functor.OplaxMonoidal.η (CategoryTheory.MonoidalOpposite.mopMopEquivalence C).inverse).unmop.unmop =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
ProfiniteAddGrp.ProfiniteCompletion.eta.eq_1 : ∀ (G : AddGrpCat),
  ProfiniteAddGrp.ProfiniteCompletion.eta G =
    AddGrpCat.ofHom { toFun := ProfiniteAddGrp.ProfiniteCompletion.etaFn G, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.RingTheory.IntegralDomain
mul_right_bijective_of_finite₀ : ∀ {M : Type u_1} [inst : MonoidWithZero M] [Finite M] [IsLeftCancelMulZero M] {a : M},
  a ≠ 0 → Function.Bijective fun b => a * b
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.range_coe_union_infty : ∀ {X : Type u_1}, Set.range OnePoint.some ∪ {OnePoint.infty} = Set.univ
-- Mathlib.Analysis.Convex.Exposed
IsExposed.mono : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : TopologicalSpace 𝕜] [inst_1 : Ring 𝕜] [inst_2 : PartialOrder 𝕜]
  [inst_3 : AddCommMonoid E] [inst_4 : TopologicalSpace E] [inst_5 : Module 𝕜 E] {A B C : Set E},
  IsExposed 𝕜 A C → B ⊆ A → C ⊆ B → IsExposed 𝕜 B C
-- Mathlib.Data.Fin.Tuple.Basic
Fin.cons_comp_succ : ∀ {n : ℕ} {α : Sort u_1} (x : α) (p : Fin n → α), Fin.cons x p ∘ Fin.succ = p
-- Lean.Parser.Extension
_private.Lean.Parser.Extension.0.Lean.Parser.ParserExtension.mkInitial : IO Lean.Parser.ParserExtension.State
-- Mathlib.RingTheory.PicardGroup
CommRing.Pic.mapAlgebra_self : ∀ {R : Type u} [inst : CommSemiring R], CommRing.Pic.mapAlgebra R R = MonoidHom.id (CommRing.Pic R)
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.eq_top_iff' : ∀ {M : Type u_1} [inst : AddZeroClass M] (S : AddSubmonoid M), S = ⊤ ↔ ∀ (x : M), x ∈ S
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsValidRevSearchFrom.below.mismatched : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice}
  {motive :
    (a : s.Pos) →
      (a_1 : List (String.Slice.Pattern.SearchStep s)) →
        String.Slice.Pattern.Model.IsValidRevSearchFrom pat a a_1 → Prop}
  {l : List (String.Slice.Pattern.SearchStep s)} {startPos endPos : s.Pos} (a : startPos < endPos)
  (a_1 : ∀ (pos : s.Pos), startPos < pos → pos ≤ endPos → ¬String.Slice.Pattern.Model.RevMatchesAt pat pos)
  (a_2 : String.Slice.Pattern.Model.IsValidRevSearchFrom pat startPos l),
  String.Slice.Pattern.Model.IsValidRevSearchFrom.below a_2 →
    motive startPos l a_2 → String.Slice.Pattern.Model.IsValidRevSearchFrom.below ⋯
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Path.nil_coe : ∀ {V : Type u} {G : SimpleGraph V} {u : V}, ↑SimpleGraph.Path.nil = SimpleGraph.Walk.nil
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
/-- Functional equation formulated for `Λ₀`.  -/
WeakFEPair.functional_equation₀ : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (P : WeakFEPair E) (s : ℂ),
  P.Λ₀ (↑P.k - s) = P.ε • P.symm.Λ₀ s
-- Init.Prelude
/-- `inferInstanceAs α` synthesizes an instance of type `α` and then adjusts it to conform to the
expected type `β`, which must be inferable from context.

Example:
```
def D := Nat
instance : Inhabited D := inferInstanceAs (Inhabited Nat)
```

The adjustment will make sure that when the resulting instance will not "leak" the RHS `Nat` when
reduced at transparency levels below `semireducible`, i.e. where `D` would not be unfolded either,
preventing "defeq abuse".

More specifically, given the "source type" (the argument) and "target type" (the expected type),
`inferInstanceAs` synthesizes an instance for the source type and then unfolds and rewraps its
components (fields, nested instances) as necessary to make them compatible with the target type. The
individual steps are represented by the following options, which all default to enabled and can be
disabled to help with porting:

* `backward.inferInstanceAs.wrap`: master switch for instance adjustment in both `inferInstanceAs`
  and the default deriving handler
* `backward.inferInstanceAs.wrap.reuseSubInstances`: reuse existing instances for the target type
  for sub-instance fields to avoid non-defeq instance diamonds
* `backward.inferInstanceAs.wrap.instances`: wrap non-reducible instances in auxiliary definitions
* `backward.inferInstanceAs.wrap.data`: wrap data fields in auxiliary definitions (proof fields are
  always wrapped)

If you just need to synthesize an instance without transporting between types, use `inferInstance`
instead, potentially with a type annotation for the expected type.
 -/
inferInstanceAs : (α : Sort u) → [i : α] → α
-- Mathlib.Tactic.Positivity.Basic
/-- Extension for `negPart`. `a⁻` is always nonnegative.  -/
Mathlib.Meta.Positivity.evalNegPart : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Data.Ordmap.Invariants
Ordnode.eraseMin.eq_def : ∀ {α : Type u_1} (x : Ordnode α),
  x.eraseMin =
    match x with
    | Ordnode.nil => Ordnode.nil
    | Ordnode.node size Ordnode.nil x r => r
    | Ordnode.node size (Ordnode.node sz l' y r') x r => (Ordnode.node sz l' y r').eraseMin.balanceR x r
-- Mathlib.Combinatorics.SimpleGraph.Dart
SimpleGraph.instDecidableEqDart.decEq : {V : Type u_2} → {G : SimpleGraph V} → [DecidableEq V] → (x x_1 : G.Dart) → Decidable (x = x_1)
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    ∀ {X : C} (f : X ⟶ T.obj₂),
      CategoryTheory.CategoryStruct.comp f T.mor₂ = 0 → ∃ g, f = CategoryTheory.CategoryStruct.comp g T.mor₁
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.sub_singleton : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Sub α] {s : Finset α} (a : α),
  s - {a} = Finset.image (fun x => x - a) s
-- Mathlib.Algebra.Tropical.Basic
Tropical.untrop_div : ∀ {R : Type u} [inst : Sub R] (x y : Tropical R), Tropical.untrop (x / y) = Tropical.untrop x - Tropical.untrop y
-- Mathlib.Order.WithBot
WithTop.coe_strictMono : ∀ {α : Type u_1} [inst : Preorder α], StrictMono fun a => ↑a
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
/-- The modification between strong transformations of oplax functors associated to a modification
between the underlying oplax transformations.  -/
CategoryTheory.Oplax.StrongTrans.Modification.mkOfOplax : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} →
          {η θ : F ⟶ G} →
            (CategoryTheory.Oplax.StrongTrans.toOplax η).Modification (CategoryTheory.Oplax.StrongTrans.toOplax θ) →
              CategoryTheory.Oplax.StrongTrans.Modification η θ
-- Mathlib.NumberTheory.LSeries.ZMod
/-- Functional equation for `ZMod` L-functions, in terms of discrete Fourier transform.  -/
ZMod.LFunction_one_sub : ∀ {N : ℕ} [inst : NeZero N] (Φ : ZMod N → ℂ) {s : ℂ},
  (∀ (n : ℕ), s ≠ -↑n) →
    Φ 0 = 0 ∨ s ≠ 1 →
      ZMod.LFunction Φ (1 - s) =
        ↑N ^ (s - 1) * (2 * ↑Real.pi) ^ (-s) * Complex.Gamma s *
          (Complex.exp (↑Real.pi * Complex.I * s / 2) * ZMod.LFunction (ZMod.dft Φ) s +
            Complex.exp (-↑Real.pi * Complex.I * s / 2) * ZMod.LFunction (ZMod.dft fun x => Φ (-x)) s)