mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Multiset.FinsetOps
Multiset.ndinter_cons_of_notMem : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} (s : Multiset α) {t : Multiset α},
  a ∉ t → (a ::ₘ s).ndinter t = s.ndinter t
-- Mathlib.Data.Nat.Cast.Basic
/-- This is primed to match `eq_intCast'`.  -/
RingHom.eq_natCast' : ∀ {R : Type u_3} [inst : NonAssocSemiring R] (f : ℕ →+* R), f = Nat.castRingHom R
-- Init.Data.SInt.Bitwise
Int16.neg_eq_not_add : ∀ (a : Int16), -a = ~~~a + 1
-- Mathlib.MeasureTheory.Group.FundamentalDomain
_private.Mathlib.MeasureTheory.Group.FundamentalDomain.0.MeasureTheory.termπ_1 : Lean.ParserDescr
-- Mathlib.Algebra.IsPrimePow
isPrimePow_nat_iff_bounded_log_minFac : ∀ (n : ℕ), IsPrimePow n ↔ ∃ k ≤ Nat.log 2 n, 0 < k ∧ n = n.minFac ^ k
-- Init.Grind.Config
Lean.Grind.NoopConfig.mk.sizeOf_spec : ∀ (toConfig : Lean.Grind.Config), sizeOf { toConfig := toConfig } = 1 + sizeOf toConfig
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Vector
Std.Iterators.Vector.isPlausibleStep_iterFromIdxM_of_not_lt : ∀ {m : Type w → Type w'} [inst : Monad m] {β : Type w} {n : ℕ} {xs : Vector β n} {pos : ℕ},
  ¬pos < n → (xs.iterFromIdxM m pos).IsPlausibleStep Std.IterStep.done
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getD_inter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {fallback : β}, (t₁ ∩ t₂).getD k fallback = if k ∈ t₂ then t₁.getD k fallback else fallback
-- Init.Data.BitVec.Bitblast
BitVec.cpopLayer.eq_1 : ∀ {len w iterNum : ℕ} (oldLayer : BitVec (len * w)) (newLayer : BitVec (iterNum * w)) (hold : 2 * (iterNum - 1) < len),
  oldLayer.cpopLayer newLayer hold =
    if hlen : len - iterNum * 2 = 0 then
      have this := ⋯;
      BitVec.cast ⋯ newLayer
    else
      have op1 := BitVec.extractLsb' (2 * iterNum * w) w oldLayer;
      have op2 := BitVec.extractLsb' ((2 * iterNum + 1) * w) w oldLayer;
      have newLayer' := op1 + op2 ++ newLayer;
      have hcast := ⋯;
      oldLayer.cpopLayer (BitVec.cast hcast newLayer') ⋯
-- Mathlib.Algebra.Lie.BaseChange
_private.Mathlib.Algebra.Lie.BaseChange.0.LieAlgebra.ExtendScalars.bracket_def : ∀ (R : Type u_1) (A : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A] [inst_3 : LieRing L] [inst_4 : LieAlgebra R L] [inst_5 : AddCommGroup M] [inst_6 : Module R M]
  [inst_7 : LieRingModule L M] [inst_8 : LieModule R L M] (x : TensorProduct R A L) (m : TensorProduct R A M),
  ⁅x, m⁆ = ((LieAlgebra.ExtendScalars.bracket'✝ R A L M) x) m
-- Batteries.Data.String.Legacy
_private.Batteries.Data.String.Legacy.0.String.set_next_add : ∀ (s : String) (i : String.Pos.Raw) (c : Char) (b₁ b₂ : ℕ),
  (String.Pos.Raw.next s i).byteIdx + b₁ = s.rawEndPos.byteIdx + b₂ →
    (String.Pos.Raw.next (String.Pos.Raw.set s i c) i).byteIdx + b₁ = (String.Pos.Raw.set s i c).rawEndPos.byteIdx + b₂
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- The underlying object in the ambient monoidal category  -/
CategoryTheory.AddGrp.X : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] → CategoryTheory.AddGrp C → C
-- Lean.Server.FileWorker.RequestHandling
Lean.Server.FileWorker.NamespaceEntry.finish : Lean.FileMap →
  Array Lean.Lsp.DocumentSymbol →
    Option Lean.Syntax → Lean.Server.FileWorker.NamespaceEntry → Array Lean.Lsp.DocumentSymbol
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.instInhabited.eq_1 : ∀ {E : Type u_3} [inst : Group E], GroupSeminorm.instInhabited = { default := 0 }
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.RightFraction.leftFraction_fac : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C}
  [inst_1 : W.HasLeftCalculusOfFractions] {X Y : C} (φ : W.RightFraction X Y),
  CategoryTheory.CategoryStruct.comp φ.f φ.leftFraction.s = CategoryTheory.CategoryStruct.comp φ.s φ.leftFraction.f
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigOWith.eventually_mul_div_cancel : ∀ {α : Type u_1} {𝕜 : Type u_15} [inst : NormedDivisionRing 𝕜] {c : ℝ} {l : Filter α} {u v : α → 𝕜},
  Asymptotics.IsBigOWith c l u v → u / v * v =ᶠ[l] u
-- Mathlib.Algebra.Group.Prod
/-- Canonical homomorphism of monoids from `αˣ` into `α × αᵐᵒᵖ`.
Used mainly to define the natural topology of `αˣ`.  -/
Units.embedProduct : (α : Type u_6) → [inst : Monoid α] → αˣ →* α × αᵐᵒᵖ
-- Mathlib.GroupTheory.GroupAction.Iwasawa
/-- The subgroups of the Iwasawa structure  -/
MulAction.IwasawaStructure.T : {M : Type u_1} →
  [inst : Group M] → {α : Type u_2} → [inst_1 : MulAction M α] → MulAction.IwasawaStructure M α → α → Subgroup M
-- Init.Data.UInt.Basic
instPowUInt64Nat : Pow UInt64 ℕ
-- Mathlib.Algebra.Homology.Embedding.Connect
CochainComplex.ConnectData.homologyMap_map_of_eq_succ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K K' : ChainComplex C ℕ} {L L' : CochainComplex C ℕ} (h : CochainComplex.ConnectData K L)
  (h' : CochainComplex.ConnectData K' L') (fK : K ⟶ K') (fL : L ⟶ L')
  (f_comm : CategoryTheory.CategoryStruct.comp (fK.f 0) h'.d₀ = CategoryTheory.CategoryStruct.comp h.d₀ (fL.f 0))
  (n : ℕ) [inst_2 : NeZero n] (m : ℤ) (hmn : m = ↑n) [inst_3 : HomologicalComplex.HasHomology h.cochainComplex m]
  [inst_4 : HomologicalComplex.HasHomology L n] [inst_5 : HomologicalComplex.HasHomology h'.cochainComplex m]
  [inst_6 : HomologicalComplex.HasHomology L' n],
  HomologicalComplex.homologyMap (h.map h' fK fL f_comm) m =
    CategoryTheory.CategoryStruct.comp (h.homologyIsoPos n m hmn).hom
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap fL n) (h'.homologyIsoPos n m hmn).inv)
-- Lean.Compiler.IR.Basic
Lean.IR.LocalContextEntry.localVar.inj : ∀ {a : Lean.IR.IRType} {a_1 : Lean.IR.Expr} {a_2 : Lean.IR.IRType} {a_3 : Lean.IR.Expr},
  Lean.IR.LocalContextEntry.localVar a a_1 = Lean.IR.LocalContextEntry.localVar a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.Algebra.Group.ULift
ULift.rightCancelMonoid : {α : Type u} → [RightCancelMonoid α] → RightCancelMonoid (ULift.{u_1, u} α)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey_erase : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {h' : a ∈ m.erase k}, (m.erase k).getKey a h' = m.getKey a ⋯
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.IsHomogeneous.map : ∀ {σ : Type u_1} {R : Type u_3} {S : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S] {φ : MvPolynomial σ R}
  {n : ℕ}, φ.IsHomogeneous n → ∀ (f : R →+* S), ((MvPolynomial.map f) φ).IsHomogeneous n
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- Characterization of the structured arrow category on the projection functor of any
structured arrow category.  -/
CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor D T) →
          (Y : T) →
            (X : D) →
              CategoryTheory.StructuredArrow X (CategoryTheory.StructuredArrow.proj Y F) ≌
                CategoryTheory.StructuredArrow Y ((CategoryTheory.Under.forget X).comp F)
-- Mathlib.InformationTheory.KullbackLeibler.KLFun
InformationTheory.klFun_one : InformationTheory.klFun 1 = 0
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.compRightId_hom : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} {f : C ⟶ C} (h : Homotopy f (CategoryTheory.CategoryStruct.id C))
  (g : C ⟶ D) (i j : ι), (h.compRightId g).hom i j = CategoryTheory.CategoryStruct.comp (h.hom i j) (g.f j)
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.ones_mul : ∀ {w : ℕ} (a : BitVec w), -1#w * a = -a
-- Std.Tactic.BVDecide.Normalize.Equal
Std.Tactic.BVDecide.Frontend.Normalize.BitVec.xor_left_inj : ∀ {w : ℕ} (a b c : BitVec w), (a ^^^ c == b ^^^ c) = (a == b)
-- Mathlib.Dynamics.PeriodicPts.Defs
/-- The period of a multiplicative action of `g` on `a` is the smallest positive `n` such that
`g ^ n • a = a`, or `0` if such an `n` does not exist.
 -/
MulAction.period : {α : Type v} → {M : Type u} → [inst : Monoid M] → [MulAction M α] → M → α → ℕ
-- Mathlib.Geometry.Manifold.StructureGroupoid
/-- A structure groupoid is a set of open partial homeomorphisms of a topological space stable under
composition and inverse. They appear in the definition of the smoothness class of a manifold.  -/
StructureGroupoid : (H : Type u_2) → [TopologicalSpace H] → Type u_2
-- Mathlib.Algebra.Module.Equiv.Basic
Units.mulLeftLinearEquiv.congr_simp : ∀ (R : Type u_9) (A : Type u_10) [inst : Semiring R] [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A], Units.mulLeftLinearEquiv R A = Units.mulLeftLinearEquiv R A
-- Mathlib.Analysis.Analytic.Constructions
AnalyticWithinAt.const_smul : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E} {x : E}
  {R : Type u_9} [inst_5 : NormedRing R] [inst_6 : Module R F] [IsBoundedSMul R F] [SMulCommClass 𝕜 R F] {c : R},
  AnalyticWithinAt 𝕜 f s x → AnalyticWithinAt 𝕜 (c • f) s x
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RoiSliceData.range : {α : Type u} → {β : Type v} → [inst : Ord α] → Std.DTreeMap.Internal.Const.RoiSliceData α β → Std.Roi α
-- Mathlib.Order.Lattice
/-- Pointwise infimum of two monotone functions is a monotone function.  -/
MonotoneOn.inf : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : SemilatticeInf β] {f g : α → β} {s : Set α},
  MonotoneOn f s → MonotoneOn g s → MonotoneOn (f ⊓ g) s
-- Init.Prelude
Nat.le.below : {n : ℕ} → {motive : (a : ℕ) → n.le a → Prop} → {a : ℕ} → n.le a → Prop
-- Mathlib.Order.Preorder.Chain
IsChain.preimage_iso : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] {t : Set β},
  IsChain (fun x1 x2 => x1 ≤ x2) t → ∀ (φ : α ≃o β), IsChain (fun x1 x2 => x1 ≤ x2) (⇑φ ⁻¹' t)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
PresheafOfModules.Sheafify.SMulCandidate.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} {α : R₀ ⟶ R.obj}
  {M₀ : PresheafOfModules R₀} {A : CategoryTheory.Sheaf J AddCommGrpCat} {φ : M₀.presheaf ⟶ A.obj} {X : Cᵒᵖ}
  {r : ↑(R.obj.obj X)} {m : ↑(A.obj.obj X)} [inst_1 : SizeOf C] (x : ↑(A.obj.obj X))
  (h :
    ∀ ⦃Y : Cᵒᵖ⦄ (f : X ⟶ Y) (r₀ : ↑(R₀.obj Y)),
      (CategoryTheory.ConcreteCategory.hom (α.app Y)) r₀ = (CategoryTheory.ConcreteCategory.hom (R.obj.map f)) r →
        ∀ (m₀ : ↑(M₀.obj Y)),
          (CategoryTheory.ConcreteCategory.hom (φ.app Y)) m₀ = (CategoryTheory.ConcreteCategory.hom (A.obj.map f)) m →
            (CategoryTheory.ConcreteCategory.hom (A.obj.map f)) x =
              (CategoryTheory.ConcreteCategory.hom (φ.app Y)) (r₀ • m₀)),
  sizeOf { x := x, h := h } = 1 + sizeOf x
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.CoPolarizationIn_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (S : Type u_5)
  [inst_5 : CommRing S] [inst_6 : Algebra S R] [inst_7 : FaithfulSMul S R] [inst_8 : Module S M] [inst_9 : Module S N]
  [inst_10 : IsScalarTower S R N] [inst_11 : P.IsValuedIn S] [inst_12 : Fintype ι] (x : ↥(P.corootSpan S)),
  (P.CoPolarizationIn S) x = ∑ i, (P.root'In S i) x • P.root i
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctorPreCore.toPrelaxFunctor : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        CategoryTheory.StrictPseudofunctorPreCore B C → CategoryTheory.PrelaxFunctor B C
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
_private.Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates.0.Tactic.ComputeAsymptotics.UnitMonomial.sign.match_1.eq_1 : ∀ (motive : Tactic.ComputeAsymptotics.UnitMonomial → Sort u_1) (h_1 : Unit → motive [])
  (h_2 : (hd : ℝ) → (tl : List ℝ) → motive (hd :: tl)),
  (match [] with
    | [] => h_1 ()
    | hd :: tl => h_2 hd tl) =
    h_1 ()
-- Mathlib.Geometry.Euclidean.SignedDist
signedDist_right_congr : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {v : V} (p : P) {q r : P},
  inner ℝ v (q -ᵥ r) = 0 → ((signedDist v) p) q = ((signedDist v) p) r
-- Mathlib.Order.Heyting.Basic
compl_compl_compl : ∀ {α : Type u_2} [inst : HeytingAlgebra α] (a : α), aᶜᶜᶜ = aᶜ
-- Init.Data.Range.Polymorphic.UInt
UInt16.instHasSize_1 : Std.Rxo.HasSize UInt16
-- Mathlib.Topology.Connected.Basic
isClosed_connectedComponent : ∀ {α : Type u} [inst : TopologicalSpace α] {x : α}, IsClosed (connectedComponent x)
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- If `B` is a `G`-block, then it is also a `H`-block for any subgroup `H` of `G`.  -/
AddAction.IsBlock.addSubgroup : ∀ {G : Type u_1} [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] {B : Set X} {H : AddSubgroup G},
  AddAction.IsBlock G B → AddAction.IsBlock (↥H) B
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
CategoryTheory.NonPreadditiveAbelian.toHasZeroMorphisms : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    [self : CategoryTheory.NonPreadditiveAbelian C] → CategoryTheory.Limits.HasZeroMorphisms C
-- Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise
ContDiffPointwiseHolderAt.comp₂_of_differentiableAt : ∀ {E : Type u_1} {F : Type u_2} {G : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G]
  {k : ℕ} {α : ↑unitInterval} (a : E) {H : Type u_4} [inst_6 : NormedAddCommGroup H] [inst_7 : NormedSpace ℝ H]
  {g : F × G → H} {f₁ : E → F} {f₂ : E → G},
  ContDiffPointwiseHolderAt k α g (f₁ a, f₂ a) →
    ContDiffPointwiseHolderAt k α f₁ a →
      ContDiffPointwiseHolderAt k α f₂ a →
        DifferentiableAt ℝ g (f₁ a, f₂ a) ∨ DifferentiableAt ℝ f₁ a ∧ DifferentiableAt ℝ f₂ a →
          ContDiffPointwiseHolderAt k α (fun x => g (f₁ x, f₂ x)) a
-- Mathlib.Algebra.Lie.Cochain
/-- Lie algebra 1-cochains over `L` with coefficients in the module `M`.  -/
LieModule.Cohomology.oneCochain : (R : Type u_1) →
  [inst : CommRing R] →
    (L : Type u_2) →
      [inst_1 : LieRing L] →
        [LieAlgebra R L] → (M : Type u_3) → [inst_3 : AddCommGroup M] → [Module R M] → Type (max u_2 u_3)
-- Mathlib.Data.PFunctor.Multivariate.W
/-- Destructor for the W-type of `P`  -/
MvPFunctor.wDest' : {n : ℕ} → (P : MvPFunctor.{u} (n + 1)) → {α : TypeVec.{u} n} → P.W α → ↑P (α ::: P.W α)
-- Mathlib.Topology.Algebra.OpenSubgroup
IsTopologicalAddGroup.addNegClosureNhd.add : ∀ {G : Type u_1} [inst : TopologicalSpace G] {T W : Set G} [inst_1 : AddGroup G],
  IsTopologicalAddGroup.addNegClosureNhd T W → W + T ⊆ W
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgHom.instCoeAlgHom : {R : Type u_2} →
  {A : Type u_3} →
    {B : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : Star A] →
              [inst_4 : Semiring B] → [inst_5 : Algebra R B] → [inst_6 : Star B] → Coe (A →⋆ₐ[R] B) (A →ₐ[R] B)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.min!_eq_getElem!_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → t.min! = t.toArray[0]!
-- Mathlib.Algebra.Polynomial.Eval.Degree
Polynomial.isUnit_of_isUnit_leadingCoeff_of_isUnit_map : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : CommRing S] [IsDomain S] (φ : R →+* S) {f : Polynomial R},
  IsUnit f.leadingCoeff → IsUnit (Polynomial.map φ f) → IsUnit f
-- Mathlib.CategoryTheory.Shift.Opposite
CategoryTheory.oppositeShiftFunctorZero_inv_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (A : Type u_2) [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (X : CategoryTheory.OppositeShift C A),
  (CategoryTheory.shiftFunctorZero (CategoryTheory.OppositeShift C A) A).inv.app X =
    ((CategoryTheory.shiftFunctorZero C A).hom.app (Opposite.unop X)).op
-- Mathlib.Order.Zorn
Flag.exists_mem : ∀ {α : Type u_1} [inst : Preorder α] (a : α), ∃ s, a ∈ s
-- Mathlib.Algebra.Group.Prod
Prod.instCommSemigroup : {G : Type u_1} → {H : Type u_2} → [CommSemigroup G] → [CommSemigroup H] → CommSemigroup (G × H)
-- Mathlib.Algebra.Group.Subgroup.Map
MulEquiv.subgroupCongr.eq_1 : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} (h : H = K),
  MulEquiv.subgroupCongr h = { toEquiv := Equiv.setCongr ⋯, map_mul' := ⋯ }
-- Mathlib.Data.Nat.Basic
Nat.two_mul_sq_add_one_le_two_pow_two_mul : ∀ (k : ℕ), 2 * k ^ 2 + 1 ≤ 2 ^ (2 * k)
-- Mathlib.Data.Fin.Tuple.Curry
Function.OfArity.curryEquiv_symm_apply : ∀ {α β : Type u} (n : ℕ) (f : Function.FromTypes (fun a => α) β) (a : Fin n → α),
  (Function.OfArity.curryEquiv n).symm f a = f.uncurry a
-- Mathlib.Algebra.WithConv
WithConv.symm_congr : ∀ {A : Type u_2} {B : Type u_3} (f : A ≃ B), (WithConv.congr f).symm = WithConv.congr f.symm
-- Init.Data.BitVec.Bitblast
BitVec.getElem_udiv : ∀ {w : ℕ} (n d : BitVec w),
  0#w < d → ∀ (i : ℕ) (hi : i < w), (n / d)[i] = (BitVec.divRec w { n := n, d := d } (BitVec.DivModState.init w)).q[i]
-- Mathlib.Algebra.Module.Presentation.Basic
/-- Given `relations : Relations A` and `solution : relations.Solution M`, this is
the canonical linear map `relations.Quotient →ₗ[A] M` from the module.  -/
Module.Relations.Solution.fromQuotient : {A : Type u} →
  [inst : Ring A] →
    {relations : Module.Relations A} →
      {M : Type v} →
        [inst_1 : AddCommGroup M] → [inst_2 : Module A M] → relations.Solution M → relations.Quotient →ₗ[A] M
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
/-- The `nonsing_inv` of `A` is a right inverse.  -/
Matrix.mul_nonsing_inv : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α),
  IsUnit A.det → A * A⁻¹ = 1
-- Mathlib.Data.Set.Lattice.Image
Set.image2_sUnion_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (s : Set α) (T : Set (Set β)),
  Set.image2 f s (⋃₀ T) = ⋃ t ∈ T, Set.image2 f s t
-- Mathlib.Algebra.Colimit.Module
DirectLimit.congr_simp : ∀ {ι : Type u_1} [inst : Preorder ι] (F : ι → Type u_4) {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8}
  (f f_1 : (i j : ι) → (h : i ≤ j) → T h) (e_f : f = f_1) [inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)]
  [inst_2 : DirectedSystem F fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι],
  DirectLimit F f = DirectLimit F f_1
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.d₁_eq_zero' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂] [inst_4 : K.HasTotal c₁₂]
  {i₁ i₁' : I₁}, c₁.Rel i₁ i₁' → ∀ (i₂ : I₂) (i₁₂ : I₁₂), c₁.π c₂ c₁₂ (i₁', i₂) ≠ i₁₂ → K.d₁ c₁₂ i₁ i₂ i₁₂ = 0
-- Mathlib.Topology.Instances.NNReal.Lemmas
Real.tendsto_toNNReal_atTop : Filter.Tendsto Real.toNNReal Filter.atTop Filter.atTop
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.HasAffineProperty.instIsZariskiLocalAtTarget : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {Q : AlgebraicGeometry.AffineTargetMorphismProperty}
  [AlgebraicGeometry.HasAffineProperty P Q], AlgebraicGeometry.IsZariskiLocalAtTarget P
-- Mathlib.Geometry.Manifold.MFDeriv.Tangent
tangentCoordChange.congr_simp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] (I I_1 : ModelWithCorners 𝕜 E H)
  (e_I : I = I_1) {M : Type u_6} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I 1 M]
  (x x_1 : M),
  x = x_1 →
    ∀ (y y_1 : M), y = y_1 → ∀ (a a_1 : M), a = a_1 → tangentCoordChange I x y a = tangentCoordChange I_1 x_1 y_1 a_1
-- Mathlib.RingTheory.MvPowerSeries.PiTopology
/-- If the order of a family of `MvPowerSeries` tends to infinity, the collection of all
possible products over `Finset` is summable.  -/
MvPowerSeries.WithPiTopology.summable_prod_of_tendsto_order_atTop_nhds_top : ∀ {σ : Type u_3} {R : Type u_4} [inst : TopologicalSpace R] [inst_1 : CommSemiring R] {ι : Type u_5}
  {f : ι → MvPowerSeries σ R} [inst_2 : LinearOrder ι] [LocallyFiniteOrderBot ι],
  Filter.Tendsto (fun i => (f i).order) Filter.atTop (nhds ⊤) → Summable fun x => ∏ i ∈ x, f i
-- Mathlib.CategoryTheory.EffectiveEpi.Enough
/-- The object of `C` giving the source of the effective epi  -/
CategoryTheory.Functor.EffectivePresentation.p : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {F : CategoryTheory.Functor C D} → {X : D} → F.EffectivePresentation X → C
-- Init.Control.Lawful.Instances
OptionT.instLawfulMonad : ∀ {m : Type u_1 → Type u_2} [inst : Monad m] [LawfulMonad m], LawfulMonad (OptionT m)
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
_private.Lean.Elab.ConfigEval.DeriveEvalConfigItem.0.Lean.Elab.ConfigEval.HandlerTrie.mk.sizeOf_spec : ∀ (exact? : Option Lean.Elab.ConfigEval.EvalConfigItemHandler)
  (children : Array (String × Lean.Elab.ConfigEval.HandlerTrie✝))
  (wildcard? : Option Lean.Elab.ConfigEval.EvalConfigItemHandler) (projFn? struct? : Option Lean.Name),
  sizeOf { exact? := exact?, children := children, wildcard? := wildcard?, projFn? := projFn?, struct? := struct? } =
    1 + sizeOf exact? + sizeOf children + sizeOf wildcard? + sizeOf projFn? + sizeOf struct?
-- Mathlib.Analysis.Complex.HasPrimitives
Complex.IsExactOn.with_val_at : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {s : Set ℂ},
  Complex.IsExactOn f s → ∀ (x₀ : ℂ) (y : E), ∃ g, g x₀ = y ∧ ∀ x ∈ s, HasDerivAt g (f x) x
-- Lean.Meta.Tactic.Simp.Main
Lean.Meta.Simp.dsimpMain : Lean.Expr →
  Lean.Meta.Simp.Context →
    optParam Lean.Meta.Simp.Stats { } →
      optParam Lean.Meta.Simp.Methods { } → Lean.MetaM (Lean.Expr × Lean.Meta.Simp.Stats)
-- Mathlib.Logic.Equiv.Defs
/-- Composition of equivalences `e₁ : α ≃ β` and `e₂ : β ≃ γ`.  -/
Equiv.trans : {α : Sort u} → {β : Sort v} → {γ : Sort w} → α ≃ β → β ≃ γ → α ≃ γ