mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.Poly.denoteN_append : ∀ {α : Type u_1} [inst : Lean.Grind.NatModule α] (ctx : Lean.Grind.Linarith.Context α)
  (p₁ p₂ : Lean.Grind.Linarith.Poly),
  p₁.NonnegCoeffs →
    p₂.NonnegCoeffs →
      Lean.Grind.Linarith.Poly.denoteN ctx (p₁.append p₂) =
        Lean.Grind.Linarith.Poly.denoteN ctx p₁ + Lean.Grind.Linarith.Poly.denoteN ctx p₂
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.weierstrassUnit_mul : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A] [inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A]
  {g g' : PowerSeries A} (hg : (PowerSeries.map (IsLocalRing.residue A)) (g * g') ≠ 0),
  (g * g').weierstrassUnit hg = g.weierstrassUnit ⋯ * g'.weierstrassUnit ⋯
-- Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
/-- If `P` holds for units and powers of primes,
and `P x ∧ P y` for coprime `x, y` implies `P (x * y)`,
then `P` holds on a product of powers of distinct primes.  -/
UniqueFactorizationMonoid.induction_on_prime_power : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [UniqueFactorizationMonoid α] {P : α → Prop} (s : Finset α) (i : α → ℕ),
  (∀ p ∈ s, Prime p) →
    (∀ p ∈ s, ∀ q ∈ s, p ∣ q → p = q) →
      (∀ {x : α}, IsUnit x → P x) →
        (∀ {p : α} (i : ℕ), Prime p → P (p ^ i)) →
          (∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)) → P (∏ p ∈ s, p ^ i p)
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.instCommSemiring : {R : Type uR} →
  {A : Type uA} →
    {B : Type uB} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : CommSemiring B] → [inst_4 : Algebra R B] → CommSemiring (TensorProduct R A B)
-- Lean.MetavarContext
Lean.MetavarKind.synthetic.sizeOf_spec : sizeOf Lean.MetavarKind.synthetic = 1
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Walk.toSubgraph_adj_iff : ∀ {V : Type u} {G : SimpleGraph V} {u v u' v' : V} (w : G.Walk u v),
  w.toSubgraph.Adj u' v' ↔ ∃ i, s(w.getVert i, w.getVert (i + 1)) = s(u', v') ∧ i < w.length
-- Mathlib.Data.Set.Lattice
Set.range_sigma_eq_iUnion_range : ∀ {α : Type u_1} {β : Type u_2} {γ : α → Type u_12} (f : Sigma γ → β), Set.range f = ⋃ a, Set.range fun b => f ⟨a, b⟩
-- Mathlib.Data.Finset.Sups
Finset.Nonempty.of_sups_right : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] {s t : Finset α}, (s ⊻ t).Nonempty → t.Nonempty
-- Init.Data.Option.Lemmas
Option.any_or_of_any_left : ∀ {α : Type u_1} {o₁ o₂ : Option α} {f : α → Bool}, Option.any f o₁ = true → Option.any f (o₁.or o₂) = true
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coconeUnopOfConeEquiv_functor_map_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} {X Y : (CategoryTheory.Limits.Cone F)ᵒᵖ} (f : X ⟶ Y),
  (CategoryTheory.Limits.coconeUnopOfConeEquiv.functor.map f).hom = f.unop.hom.unop
-- Mathlib.Data.LawfulXor.Equiv
Equiv.xor_apply : ∀ {α : Type u_1} [inst : XorOp α] [inst_1 : Zero α] [inst_2 : LawfulXor α] (a x : α), (Equiv.xor a) x = a ^^^ x
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.containsAtAux : {α : Type u_1} → {β : Type u_2} → [BEq α] → (keys : Array α) → (vals : Array β) → keys.size = vals.size → ℕ → α → Bool
-- Batteries.Data.Array.Merge
_private.Batteries.Data.Array.Merge.0.Array.mergeDedupWith.go.match_1.eq_3 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.gt)
  (h_3 : Unit → motive Ordering.eq),
  (match Ordering.eq with
    | Ordering.lt => h_1 ()
    | Ordering.gt => h_2 ()
    | Ordering.eq => h_3 ()) =
    h_3 ()
-- Lean.Meta.SynthInstance
/-- Move waiters that are waiting for the given answer to the resume stack.  -/
Lean.Meta.SynthInstance.wakeUp : Lean.Meta.SynthInstance.Answer → Lean.Meta.SynthInstance.Waiter → Lean.Meta.SynthInstance.SynthM Unit
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.MonObj.lift_comp_one_right : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : C} [inst_2 : CategoryTheory.MonObj B] (f : A ⟶ B) (g : A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift f (CategoryTheory.CategoryStruct.comp g CategoryTheory.MonObj.one))
      CategoryTheory.MonObj.mul =
    f
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.Measure.m_iUnion : ∀ {α : Type u_6} [inst : MeasurableSpace α] (self : MeasureTheory.Measure α) ⦃f : ℕ → Set α⦄,
  (∀ (i : ℕ), MeasurableSet (f i)) →
    Pairwise (Function.onFun Disjoint f) → self.toOuterMeasure (⋃ i, f i) = ∑' (i : ℕ), self.toOuterMeasure (f i)
-- Init.Data.Dyadic.Basic
_private.Init.Data.Dyadic.Basic.0.Dyadic.add.match_3.splitter : (motive : Dyadic → Dyadic → Sort u_1) →
  (x y : Dyadic) →
    ((y : Dyadic) → motive Dyadic.zero y) →
      ((x : Dyadic) → (x = Dyadic.zero → False) → motive x Dyadic.zero) →
        ((n₁ k₁ : ℤ) →
            (hn₁ : n₁ % 2 = 1) →
              (n₂ k₂ : ℤ) → (hn₂ : n₂ % 2 = 1) → motive (Dyadic.ofOdd n₁ k₁ hn₁) (Dyadic.ofOdd n₂ k₂ hn₂)) →
          motive x y
-- Mathlib.Algebra.Homology.ImageToKernel
imageToKernel'_kernelSubobjectIso : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V}
  (f : A ⟶ B) (g : B ⟶ C) [inst_2 : CategoryTheory.Limits.HasKernels V] [inst_3 : CategoryTheory.Limits.HasImages V]
  (w : CategoryTheory.CategoryStruct.comp f g = 0),
  CategoryTheory.CategoryStruct.comp (imageToKernel' f g w) (CategoryTheory.Limits.kernelSubobjectIso g).inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectIso f).inv (imageToKernel f g w)
-- Mathlib.Analysis.InnerProductSpace.Subspace
OrthogonalFamily.norm_sum : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {G : ι → Type u_5} [inst_3 : (i : ι) → NormedAddCommGroup (G i)]
  [inst_4 : (i : ι) → InnerProductSpace 𝕜 (G i)] {V : (i : ι) → G i →ₗᵢ[𝕜] E},
  OrthogonalFamily 𝕜 G V → ∀ (l : (i : ι) → G i) (s : Finset ι), ‖∑ i ∈ s, (V i) (l i)‖ ^ 2 = ∑ i ∈ s, ‖l i‖ ^ 2
-- Mathlib.Analysis.Convex.Deriv
ConvexOn.monotoneOn_slope_lt : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜} {x : 𝕜},
  ConvexOn 𝕜 s f → x ∈ s → MonotoneOn (slope f x) {y | y ∈ s ∧ y < x}
-- Mathlib.Combinatorics.Matroid.Basic
_private.Mathlib.Combinatorics.Matroid.Basic.0.Matroid.subset_ground_of_subset : ∀ {α : Type u_1} {M : Matroid α} {X Y : Set α}, X ⊆ Y → Y ⊆ M.E → X ⊆ M.E
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.disjoint_coe_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α] (K L : TopologicalSpace.Compacts α), Disjoint ↑K ↑L ↔ Disjoint K L
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getD_toArray_rio : ∀ {n i fallback : ℕ}, (*...n).toArray.getD i fallback = if i < n then i else fallback
-- Std.Http.Data.URI.Basic
Std.Http.URI.instReprAuthority : Repr Std.Http.URI.Authority
-- Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
AlgebraicGeometry.Scheme.IdealSheafData.support_map : ∀ {X Y : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (f : X ⟶ Y) [AlgebraicGeometry.QuasiCompact f],
  (I.map f).support = TopologicalSpace.Closeds.closure (⇑f '' ↑I.support)
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.epi_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.IsGrothendieckAbelian.{w, v, u} C] {X : C} {J : Type w}
  [inst_3 : CategoryTheory.SmallCategory J] {Y : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone Y}
  (hc : CategoryTheory.Limits.IsColimit c) (z : X ⟶ c.pt) [CategoryTheory.IsFiltered J],
  CategoryTheory.Epi (CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.f z)
-- Init.Data.UInt.Lemmas
UInt16.lt_of_le_of_ne : ∀ {a b : UInt16}, a ≤ b → a ≠ b → a < b
-- Mathlib.Probability.Process.Adapted
MeasureTheory.IsProgressive.sub : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} {u v : ι → Ω → β} {mi : MeasurableSpace ι} {mβ : MeasurableSpace β} [inst_1 : AddGroup β]
  [MeasurableSub₂ β],
  MeasureTheory.IsProgressive f u →
    MeasureTheory.IsProgressive f v → MeasureTheory.IsProgressive f fun i ω => u i ω - v i ω
-- Mathlib.CategoryTheory.Adjunction.Limits
/-- The left adjoint of `Cone.functoriality K G : Cone K ⥤ Cone (K ⋙ G)`.

Auxiliary definition for `functorialityAdjunction'`.
 -/
CategoryTheory.Adjunction.functorialityLeftAdjoint : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            (F ⊣ G) →
              {J : Type u} →
                [inst_2 : CategoryTheory.Category.{v, u} J] →
                  (K : CategoryTheory.Functor J D) →
                    CategoryTheory.Functor (CategoryTheory.Limits.Cone (K.comp G)) (CategoryTheory.Limits.Cone K)
-- Lean.Elab.ConfigEval.Types
/-- Whether this was using `+`/`-`, to be able to give a better error message on type mismatch.
It also caches the value so we can skip evaluation for `Bool`, which is a very common case.  -/
Lean.Elab.ConfigEval.ConfigItem.bool? : Lean.Elab.ConfigEval.ConfigItem → Option Bool
-- Mathlib.Algebra.Order.Group.PosPart
leOnePart_eq_inv_inf_one : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] [MulLeftMono α] [MulRightMono α] (a : α), a⁻ᵐ = (a ⊓ 1)⁻¹
-- Lean.Meta.Tactic.LibrarySearch
Lean.Meta.LibrarySearch.DeclMod.mpr.sizeOf_spec : sizeOf Lean.Meta.LibrarySearch.DeclMod.mpr = 1
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.term.eq_1 : ∀ (I : Type u) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}}
  (ho : o < Ordinal.type fun x1 x2 => x1 < x2),
  Profinite.NobelingProof.term I ho = (Ordinal.enum fun x1 x2 => x1 < x2) ⟨o, ho⟩
-- Std.Async.System
/-- OS name.
 -/
Std.Async.System.OSInfo.name : Std.Async.System.OSInfo → String
-- Init.Control.Do
/-- A specialization of `Except.casesOn`.  -/
EarlyReturn.runK : {ρ α : Type u} → {β : Type v} → Except ρ α → (ρ → β) → (α → β) → β
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.isRegular_preAleph_succ : ∀ {o : Ordinal.{u_1}}, Ordinal.omega0 ≤ o → (Cardinal.preAleph (Order.succ o)).IsRegular
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
Subgroup.op_injective : ∀ {G : Type u_2} [inst : Group G], Function.Injective Subgroup.op
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.comp_base : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [inst_6 : CategoryTheory.Category.{v₇, u₇} A'']
  [inst_7 : CategoryTheory.Category.{v₈, u₈} B''] [inst_8 : CategoryTheory.Category.{v₉, u₉} C'']
  {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''}
  (ψ : CategoryTheory.Limits.CatCospanTransform F G F' G')
  (ψ' : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''), (ψ.comp ψ').base = ψ.base.comp ψ'.base
-- Mathlib.Topology.Compactness.Compact
CompactSpace.elim_nhds_subcover : ∀ {X : Type u} [inst : TopologicalSpace X] [CompactSpace X] (U : X → Set X),
  (∀ (x : X), U x ∈ nhds x) → ∃ t, ⋃ x ∈ t, U x = ⊤
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.alter!.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.LawfulEqOrd α] (k : α)
  (f f_1 : Option (β k) → Option (β k)),
  f = f_1 →
    ∀ (t t_1 : Std.DTreeMap.Internal.Impl α β),
      t = t_1 → Std.DTreeMap.Internal.Impl.alter! k f t = Std.DTreeMap.Internal.Impl.alter! k f_1 t_1
-- Init.Data.SInt.Basic
instMaxInt64 : Max Int64
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.eta_inv_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} (f : CategoryTheory.CostructuredArrow S T),
  f.eta.inv.left = CategoryTheory.CategoryStruct.id f.left
-- Mathlib.Order.PiLex
Pi.Lex.noMaxOrder' : ∀ {ι : Type u_1} {β : ι → Type u_2} [inst : Preorder ι] [inst_1 : (i : ι) → LT (β i)] (i : ι) [NoMaxOrder (β i)],
  NoMaxOrder (Lex ((i : ι) → β i))
-- Mathlib.Analysis.Normed.Module.Basic
MulOpposite.instNormedAlgebra : (𝕜 : Type u_1) →
  [inst : NormedField 𝕜] → {E : Type u_6} → [inst_1 : SeminormedRing E] → [NormedAlgebra 𝕜 E] → NormedAlgebra 𝕜 Eᵐᵒᵖ
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
/-- We say that a real number `x` is a Liouville number with exponent `p : ℝ` if there exists a real
number `C` such that for infinitely many denominators `n` there exists a numerator `m` such that
`x ≠ m / n` and `|x - m / n| < C / n ^ p`.

A number is a Liouville number in the sense of `Liouville` if it is `LiouvilleWith` any real
exponent.  -/
LiouvilleWith : ℝ → ℝ → Prop
-- Mathlib.Analysis.Meromorphic.Order
/-- A meromorphic function converges to zero iff its order is positive.  -/
tendsto_zero_iff_meromorphicOrderAt_pos : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜},
  MeromorphicAt f x → (Filter.Tendsto f (nhdsWithin x {x}ᶜ) (nhds 0) ↔ 0 < meromorphicOrderAt f x)
-- Mathlib.Algebra.Order.Group.Indicator
Set.indicator_le_indicator : ∀ {α : Type u_2} {M : Type u_3} [inst : Preorder M] [inst_1 : Zero M] {s : Set α} {f g : α → M} {a : α},
  f a ≤ g a → s.indicator f a ≤ s.indicator g a
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproductUniqueIso_inv : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_2 : Unique J] (f : J → C),
  (CategoryTheory.Limits.biproductUniqueIso f).inv =
    CategoryTheory.Limits.biproduct.lift (CategoryTheory.Limits.limitBiconeOfUnique f).bicone.π
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrpObj.add_neg_rev : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (G : C) [inst_3 : CategoryTheory.AddGrpObj G],
  CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add CategoryTheory.AddGrpObj.neg =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddGrpObj.neg CategoryTheory.AddGrpObj.neg)
      (CategoryTheory.CategoryStruct.comp (β_ G G).hom CategoryTheory.AddMonObj.add)
-- Std.Time.Zoned
/-- Get the current time, in the local timezone.
To obtain the current time in a specific timezone, use `DateTime.now` or `DateTime.nowAt`.
 -/
Std.Time.PlainDateTime.now : IO Std.Time.PlainDateTime
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.associator_inv_app : ∀ {B C D E : CategoryTheory.Cat} (F : B ⟶ C) (G : C ⟶ D) (H : D ⟶ E) (X : ↑B),
  (CategoryTheory.Bicategory.associator F G H).inv.toNatTrans.app X = CategoryTheory.eqToHom ⋯
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
UniformOnFun.uniformContinuous_eval_of_mem_sUnion : ∀ {α : Type u_1} (β : Type u_2) [inst : UniformSpace β] (𝔖 : Set (Set α)) {x : α},
  x ∈ ⋃₀ 𝔖 → UniformContinuous (Function.eval x ∘ ⇑(UniformOnFun.toFun 𝔖))
-- Mathlib.Analysis.Normed.Group.Basic
/-- **Alias** of the reverse direction of `nontrivialTopology_iff_exists_nnnorm_ne_zero'`. -/
NontrivialTopology.of_exists_nnnorm_ne_zero' : ∀ {E : Type u_5} [inst : SeminormedGroup E], (∃ x, ‖x‖₊ ≠ 0) → NontrivialTopology E
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the reverse direction of `Asymptotics.isBigOWith_neg_left`. -/
Asymptotics.IsBigOWith.neg_left : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {c : ℝ} {g : α → F}
  {f' : α → E'} {l : Filter α}, Asymptotics.IsBigOWith c l f' g → Asymptotics.IsBigOWith c l (fun x => -f' x) g
-- Mathlib.Algebra.Algebra.Opposite
AlgEquiv.op_symm_apply_symm_apply : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) (a : B),
  (AlgEquiv.op.symm f).symm a = MulOpposite.unop (f.symm (MulOpposite.op a))
-- Mathlib.Analysis.LocallyConvex.AbsConvexOpen
gaugeSeminorm.congr_simp : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s s_1 : Set E} (e_s : s = s_1)
  [inst_2 : RCLike 𝕜] [inst_3 : Module 𝕜 E] [inst_4 : IsScalarTower ℝ 𝕜 E] (hs₀ : Balanced 𝕜 s) (hs₁ : Convex ℝ s)
  (hs₂ : Absorbent ℝ s), gaugeSeminorm hs₀ hs₁ hs₂ = gaugeSeminorm ⋯ ⋯ ⋯
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.forM_eq_forMUncurried : ∀ {α : Type u} {cmp : α → α → Ordering} {m : Type w → Type w'} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp}
  [inst : Monad m] [LawfulMonad m] {f : α → β → m PUnit.{w + 1}},
  Std.DTreeMap.forM f t = Std.DTreeMap.Const.forMUncurried (fun a => f a.1 a.2) t
-- Mathlib.Order.Partition.Finpartition
Finpartition.parts_extendOfLE_of_eq : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] [inst_1 : DecidableEq α] {a b : α} (P : Finpartition a)
  (hab : a = b), (P.extendOfLE ⋯).parts = P.parts
-- Lean.Data.Lsp.Workspace
Lean.Lsp.FileChangeType.Changed : Lean.Lsp.FileChangeType
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.Expr.denote.match_1.eq_1 : ∀ (motive : Int.Internal.Linear.Expr → Sort u_1) (a b : Int.Internal.Linear.Expr)
  (h_1 : (a b : Int.Internal.Linear.Expr) → motive (a.add b))
  (h_2 : (a b : Int.Internal.Linear.Expr) → motive (a.sub b)) (h_3 : (a : Int.Internal.Linear.Expr) → motive a.neg)
  (h_4 : (k : ℤ) → motive (Int.Internal.Linear.Expr.num k))
  (h_5 : (v : Int.Internal.Linear.Var) → motive (Int.Internal.Linear.Expr.var v))
  (h_6 : (k : ℤ) → (e : Int.Internal.Linear.Expr) → motive (Int.Internal.Linear.Expr.mulL k e))
  (h_7 : (e : Int.Internal.Linear.Expr) → (k : ℤ) → motive (e.mulR k)),
  (match a.add b with
    | a.add b => h_1 a b
    | a.sub b => h_2 a b
    | a.neg => h_3 a
    | Int.Internal.Linear.Expr.num k => h_4 k
    | Int.Internal.Linear.Expr.var v => h_5 v
    | Int.Internal.Linear.Expr.mulL k e => h_6 k e
    | e.mulR k => h_7 e k) =
    h_1 a b
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.evaluationUncurried_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (p : C × CategoryTheory.Functor C D), (CategoryTheory.evaluationUncurried C D).obj p = p.2.obj p.1
-- Std.Data.HashMap.Lemmas
Std.HashMap.getD_insert_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α}
  {fallback v : β}, (m.insert k v).getD k fallback = v
-- Mathlib.Algebra.Order.Group.Ideal
/-- In a canonically ordered and well-quasi-ordered monoid, any semigroup ideal is finitely
generated.  -/
SemigroupIdeal.fg_of_wellQuasiOrderedLE : ∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : PartialOrder M] [WellQuasiOrderedLE M] [CanonicallyOrderedMul M]
  (I : SemigroupIdeal M), I.FG
-- Mathlib.GroupTheory.PresentedGroup
PresentedGroup.toGroup.unique : ∀ {α : Type u_1} {G : Type u_3} [inst : Group G] {f : α → G} {rels : Set (FreeGroup α)}
  (h : ∀ r ∈ rels, (FreeGroup.lift f) r = 1) (g : PresentedGroup rels →* G),
  (∀ (x : α), g (PresentedGroup.of x) = f x) → ∀ {x : PresentedGroup rels}, g x = (PresentedGroup.toGroup h) x
-- Lean.Elab.Binders
_private.Lean.Elab.Binders.0.Lean.Elab.Term.registerFailedToInferBinderTypeInfo : Lean.Expr → Lean.Elab.Term.BinderView → Lean.Elab.TermElabM Unit
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.const_add_term : ∀ {α : Type u_1} [inst : AddCommMonoid α] (k : α) (n : ℕ) (x a a' : α),
  k + a = a' → k + Mathlib.Tactic.Abel.term n x a = Mathlib.Tactic.Abel.term n x a'
-- Std.Net.Addr
Std.Net.instDecidableEqSocketAddressV4.decEq : (x x_1 : Std.Net.SocketAddressV4) → Decidable (x = x_1)
-- Batteries.Data.Fin.Lemmas
Fin.get_findRev?_eq_true : ∀ {n : ℕ} {p : Fin n → Bool} (h : (Fin.findRev? p).isSome = true), p ((Fin.findRev? p).get h) = true
-- Std.Http.Data.Headers
/-- Maps a function over all header values, producing new headers.
 -/
Std.Http.Headers.mapValues : Std.Http.Headers → (Std.Http.Header.Name → Std.Http.Header.Value → Std.Http.Header.Value) → Std.Http.Headers
-- Mathlib.GroupTheory.QuotientGroup.Basic
/-- Let `A', A, B', B` be subgroups of `G`.
If `A' = B'` and `A = B`, then the quotients `A / (A' ⊓ A)` and `B / (B' ⊓ B)` are isomorphic.

Applying this equiv is nicer than rewriting along the equalities, since the type of
`(A'.subgroupOf A : Subgroup A)` depends on `A`.
 -/
QuotientGroup.equivQuotientSubgroupOfOfEq : {G : Type u} →
  [inst : Group G] →
    {A' A B' B : Subgroup G} →
      [hAN : (A'.subgroupOf A).Normal] →
        [hBN : (B'.subgroupOf B).Normal] → A' = B' → A = B → ↥A ⧸ A'.subgroupOf A ≃* ↥B ⧸ B'.subgroupOf B
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.sInf_compl_lt_ord_succ : ∀ {ι : Type u} (f : ι → Ordinal.{u}), sInf (Set.range f)ᶜ < (Order.succ (Cardinal.mk ι)).ord
-- Mathlib.Analysis.Seminorm
Seminorm.continuous_of_le : ∀ {𝕝 : Type u_6} {E : Type u_7} [inst : SeminormedRing 𝕝] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕝 E]
  [inst_3 : TopologicalSpace E] [IsTopologicalAddGroup E] {p q : Seminorm 𝕝 E}, Continuous ⇑q → p ≤ q → Continuous ⇑p
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.map_zero : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  {P' : Type u_3} [inst_3 : CommRing P'] [inst_4 : Algebra R P'] (g : P →ₐ[R] P'), FractionalIdeal.map g 0 = 0
-- Mathlib.RingTheory.LocalRing.RingHom.Basic
RingEquiv.isLocalRing : ∀ {A : Type u_4} {B : Type u_5} [inst : CommSemiring A] [IsLocalRing A] [inst_2 : Semiring B] (e : A ≃+* B),
  IsLocalRing B
-- Lean.Elab.PreDefinition.Structural.IndGroupInfo
Lean.Elab.Structural.IndGroupInfo.mk : Array Lean.Name → ℕ → Lean.Elab.Structural.IndGroupInfo
-- Mathlib.Algebra.Category.Grp.FilteredColimits
CommGrpCat.FilteredColimits.colimit.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J CommGrpCat),
  CommGrpCat.FilteredColimits.colimit F = CommGrpCat.of ↑(CommGrpCat.FilteredColimits.G F)
-- Mathlib.Algebra.Category.Ring.Under.Basic
/-- Turn a morphism in `Under R` into an algebra homomorphism.  -/
CommRingCat.toAlgHom : {R : CommRingCat} → {A B : CategoryTheory.Under R} → (A ⟶ B) → ↑A.right →ₐ[↑R] ↑B.right
-- Mathlib.CategoryTheory.Subobject.HasCardinalLT
CategoryTheory.Subobject.hasCardinalLT_of_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {Y : C} {κ : Cardinal.{w}},
  HasCardinalLT (CategoryTheory.Subobject Y) κ →
    ∀ {X : C} (f : X ⟶ Y) [CategoryTheory.Mono f], HasCardinalLT (CategoryTheory.Subobject X) κ
-- Mathlib.GroupTheory.Commutator.Basic
commutatorElement_mul_right_mul : ∀ {G : Type u_1} [inst : Group G] (a b c : G), ⁅a, b * c⁆ * ⁅b, c * a⁆ * ⁅c, a * b⁆ = 1
-- Mathlib.Algebra.Group.Units.Hom
isUnit_map_iff : ∀ {R : Type u_2} {S : Type u_3} {F : Type u_5} [inst : Monoid R] [inst_1 : Monoid S] [inst_2 : FunLike F R S]
  [MonoidHomClass F R S] (f : F) [IsLocalHom f] (a : R), IsUnit (f a) ↔ IsUnit a
-- Lean.Meta.Tactic.Grind.AC.Seq
Lean.Grind.AC.instOrdSeq_lean : Ord Lean.Grind.AC.Seq
-- Mathlib.SetTheory.ZFC.Rank
PSet.le_succ_rank_sUnion : ∀ (x : PSet.{u_1}), x.rank ≤ Order.succ (⋃₀ x).rank