mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.ArithmeticFunction.LFunction
/-- If arithmetic functions `f i` converges to `1` pointwise, then the partial products
`∏ i ∈ s, f i` converge to `eulerProduct f` pointwise.  -/
ArithmeticFunction.tendsTo_eulerProduct_of_tendsTo : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommSemiring R] (f : ι → ArithmeticFunction R),
  (∀ (n : ℕ), ∀ᶠ (i : ι) in Filter.cofinite, (f i) n = 1 n) →
    ∀ (n : ℕ), ∀ᶠ (s : Finset ι) in Filter.atTop, (∏ i ∈ s, f i) n = (ArithmeticFunction.eulerProduct f) n
-- Init.Data.Range.Polymorphic.Iterators
/-- Returns the number of elements contained in the given left-open right-unbounded range.
 -/
Std.Roi.size : {α : Type u} → [Std.Rxi.HasSize α] → [Std.PRange.UpwardEnumerable α] → Std.Roi α → ℕ
-- Lean.Setup
Lean.IRPhases.all.sizeOf_spec : sizeOf Lean.IRPhases.all = 1
-- Mathlib.Data.ZMod.Units
ZMod.unitOfIsCoprime.congr_simp : ∀ {m : ℕ} (n n_1 : ℤ) (e_n : n = n_1) (h : IsCoprime n ↑m), ZMod.unitOfIsCoprime n h = ZMod.unitOfIsCoprime n_1 ⋯
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteArchimedeanClass.mk_le_mk : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {a : M} (ha : a ≠ 0)
  {b : M} (hb : b ≠ 0),
  FiniteArchimedeanClass.mk a ha ≤ FiniteArchimedeanClass.mk b hb ↔ ArchimedeanClass.mk a ≤ ArchimedeanClass.mk b
-- Mathlib.Logic.Function.Basic
Function.invFun_neg : ∀ {α : Sort u_1} {β : Sort u_2} [inst : Nonempty α] {f : α → β} {b : β},
  (¬∃ a, f a = b) → Function.invFun f b = Classical.choice inst
-- Mathlib.Data.Multiset.NatAntidiagonal
/-- The cardinality of the antidiagonal of `n` is `n+1`.  -/
Multiset.Nat.card_antidiagonal : ∀ (n : ℕ), (Multiset.Nat.antidiagonal n).card = n + 1
-- Mathlib.Analysis.Meromorphic.Basic
MeromorphicOn.mul : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {s t : 𝕜 → 𝕜'} {U : Set 𝕜},
  MeromorphicOn s U → MeromorphicOn t U → MeromorphicOn (s * t) U
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.coe_support_append' : ∀ {V : Type u} {G : SimpleGraph V} [inst : DecidableEq V] {u v w : V} (p : G.Walk u v) (p' : G.Walk v w),
  ↑(p.append p').support = ↑p.support + ↑p'.support - {v}
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.WorkspaceSymbolParams.mk : String → Lean.Lsp.WorkspaceSymbolParams
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.closure_disjoint_coloops_of_disjoint_coloops : ∀ {α : Type u_1} {M : Matroid α} {X : Set α}, Disjoint X M.coloops → Disjoint (M.closure X) M.coloops
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
CategoryTheory.Limits.HasZeroObject.to_zero_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C] {X : C}
  (f g : X ⟶ 0), f = g
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.AECover.inter_restrict : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι} {φ : ι → Set α},
  MeasureTheory.AECover μ l φ → ∀ {s : Set α}, MeasurableSet s → MeasureTheory.AECover (μ.restrict s) l fun i => φ i ∩ s
-- Mathlib.RingTheory.Valuation.Basic
/-- The `AddValuation` associated to a `Valuation`.  -/
Valuation.toAddValuation : {R : Type u_3} →
  {Γ₀ : Type u_5} →
    [inst : Ring R] → [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] → Valuation R Γ₀ ≃ AddValuation R (Additive Γ₀)ᵒᵈ
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.List.anyM.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match true with
    | true => h_1 ()
    | false => h_2 ()) =
    h_1 ()
-- Init.Grind.Ordered.Rat
Lean.Grind.instOrderedAddRat : Lean.Grind.OrderedAdd ℚ
-- Mathlib.Order.Sublocale
/-- See `Sublocale.restrict` for the public-facing version.  -/
_private.Mathlib.Order.Sublocale.0.Sublocale.restrictAux : {X : Type u_1} → [inst : Order.Frame X] → (S : Sublocale X) → X → ↥S
-- Mathlib.Topology.Covering.Quotient
Topology.IsQuotientMap.trivializationOfVAddDisjoint_baseSet : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {G : Type u_3}
  [inst_2 : AddGroup G] [inst_3 : AddAction G E] (hf : Topology.IsQuotientMap f) [inst_4 : ContinuousConstVAdd G E]
  (hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ AddAction.orbit G e₂) [inst_5 : TopologicalSpace G]
  [inst_6 : DiscreteTopology G] (U : Set E) (open_U : IsOpen U)
  (disjoint : ∀ (g : G), ((fun x => g +ᵥ x) '' U ∩ U).Nonempty → g = 0),
  (hf.trivializationOfVAddDisjoint hfG U open_U disjoint).baseSet = f '' U
-- Mathlib.Analysis.Meromorphic.Basic
/-- Eta-expanded form of `Meromorphic.div` -/
Meromorphic.fun_div : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {f g : 𝕜 → 𝕜'}, Meromorphic f → Meromorphic g → Meromorphic fun i => f i / g i
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasurableEmbedding.eLpNormEssSup_map_measure : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε : Type u_7} [inst : TopologicalSpace ε]
  [inst_1 : ContinuousENorm ε] {β : Type u_8} {mβ : MeasurableSpace β} {f : α → β} {g : β → ε},
  MeasurableEmbedding f →
    MeasureTheory.eLpNormEssSup g (MeasureTheory.Measure.map f μ) = MeasureTheory.eLpNormEssSup (g ∘ f) μ
-- Mathlib.Data.Fintype.Perm
_private.Mathlib.Data.Fintype.Perm.0.permsOfList.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (a : α) (l : List α) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (l : List α) → motive (a :: l)),
  (match a :: l with
    | [] => h_1 ()
    | a :: l => h_2 a l) =
    h_2 a l
-- Mathlib.Algebra.Group.Defs
_private.Mathlib.Algebra.Group.Defs.0.npowRec'.match_1.splitter : {M : Type u_2} →
  (motive : ℕ → M → Sort u_1) →
    (x : ℕ) →
      (x_1 : M) →
        ((x : M) → motive 0 x) → ((m : M) → motive 1 m) → ((k : ℕ) → (m : M) → motive k.succ.succ m) → motive x x_1
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Filtered
CategoryTheory.Limits.has_filtered_colimits_of_has_cofiltered_limits_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [CategoryTheory.Limits.HasCofilteredLimitsOfSize.{v₂, u₂, v₁, u₁} Cᵒᵖ],
  CategoryTheory.Limits.HasFilteredColimitsOfSize.{v₂, u₂, v₁, u₁} C
-- Mathlib.RepresentationTheory.Homological.TateCohomology.Basic
tateComplex.map_add : ∀ {R G : Type u} [inst : CommRing R] [inst_1 : Group G] [inst_2 : Fintype G] {X Y : Rep.{u, u, u} R G} (f g : X ⟶ Y),
  tateComplex.map (f + g) = tateComplex.map f + tateComplex.map g
-- Init.Data.Int.LemmasAux
Int.neg_ofNat_le_natCast : ∀ (n m : ℕ), -OfNat.ofNat n ≤ ↑m
-- Mathlib.MeasureTheory.Measure.Count
MeasureTheory.count_real_singleton : ∀ {α : Type u_1} [inst : MeasurableSpace α] [MeasurableSingletonClass α] (a : α),
  MeasureTheory.Measure.count.real {a} = 1
-- Aesop.Script.StructureDynamic
Aesop.Script.UScript.toSScriptDynamic : Lean.Meta.SavedState → Lean.MVarId → Aesop.Script.UScript → Lean.MetaM (Option (Aesop.Script.SScript × Bool))
-- Mathlib.Data.Rat.Init
/-- Rational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
 -/
termℚ : Lean.ParserDescr
-- Lean.Parser.Extra
Lean.Parser.strLit.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Order.Max
IsBot.not_isTop : ∀ {α : Type u_1} [inst : PartialOrder α] {a : α} [Nontrivial α], IsBot a → ¬IsTop a
-- Mathlib.Data.LawfulXor.Equiv
Equiv.xor_eq_one_iff : ∀ {α : Type u_1} [inst : XorOp α] [inst_1 : Zero α] [inst_2 : LawfulXor α] {a : α}, Equiv.xor a = 1 ↔ a = 0
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- Predicate asserting that the word `L` admits no reduction steps, i.e., no two neighboring
elements of the word cancel.  -/
FreeGroup.IsReduced : {α : Type u} → List (α × Bool) → Prop
-- Mathlib.Topology.IsLocalHomeomorph
/-- Continuous local sections of a local homeomorphism are open embeddings.  -/
IsLocalHomeomorph.isOpenEmbedding_of_comp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {g : Y → Z} {f : X → Y},
  IsLocalHomeomorph g → Topology.IsOpenEmbedding (g ∘ f) → Continuous f → Topology.IsOpenEmbedding f
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getD_diff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α} {fallback : β}, (t₁ \ t₂).getD k fallback = if k ∈ t₂ then fallback else t₁.getD k fallback
-- Mathlib.Algebra.Category.BialgCat.Basic
BialgCat.mk.inj : ∀ {R : Type u} {inst : CommRing R} {carrier : Type v} {instRing : Ring carrier} {instBialgebra : Bialgebra R carrier}
  {carrier_1 : Type v} {instRing_1 : Ring carrier_1} {instBialgebra_1 : Bialgebra R carrier_1},
  { carrier := carrier, instRing := instRing, instBialgebra := instBialgebra } =
      { carrier := carrier_1, instRing := instRing_1, instBialgebra := instBialgebra_1 } →
    carrier = carrier_1 ∧ instRing ≍ instRing_1 ∧ instBialgebra ≍ instBialgebra_1
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Simprocs.erased : Lean.Meta.Simprocs → Lean.PHashSet Lean.Name
-- Mathlib.Topology.MetricSpace.HausdorffDistance
Metric.disjoint_ball_infDist : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {x : α}, Disjoint (Metric.ball x (Metric.infDist x s)) s
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.mapOfLE.congr_simp : ∀ {K : Type u} [inst : Field K] (R S : ValuationSubring K) (h : R ≤ S), R.mapOfLE S h = R.mapOfLE S h
-- Lean.Attributes
Lean.Attribute.Builtin.getId : Lean.Syntax → Lean.AttrM Lean.Name
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.Monic.supDegree_mul : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : LinearOrder B] [inst_2 : OrderBot B]
  {p q : AddMonoidAlgebra R A} {D : A → B} [inst_3 : AddZeroClass A] [inst_4 : Add B] [AddLeftStrictMono B]
  [AddRightStrictMono B],
  Function.Injective D →
    (∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) →
      ⊥ + ⊥ = ⊥ →
        AddMonoidAlgebra.Monic D p →
          AddMonoidAlgebra.Monic D q →
            AddMonoidAlgebra.supDegree D (p * q) = AddMonoidAlgebra.supDegree D p + AddMonoidAlgebra.supDegree D q
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec64_add : ∀ {a b : ISize} (h : System.Platform.numBits = 64), (a + b).toBitVec64 h = a.toBitVec64 h + b.toBitVec64 h
-- Mathlib.Combinatorics.Matroid.Circuit
/-- The circuit elimination axiom : for any pair of distinct circuits `C₁, C₂` and any `e`,
some circuit is contained in `(C₁ ∪ C₂) \ {e}`.

This is one of the axioms when defining a finitary matroid via circuits;
as an axiom, it is usually stated with the extra assumption that `e ∈ C₁ ∩ C₂`.  -/
Matroid.IsCircuit.elimination : ∀ {α : Type u_1} {M : Matroid α} {C₁ C₂ : Set α},
  M.IsCircuit C₁ → M.IsCircuit C₂ → C₁ ≠ C₂ → ∀ (e : α), ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.instSupSet : {E : Type u_3} → [inst : AddGroup E] → SupSet (AddGroupSeminorm E)
-- Mathlib.Algebra.Order.Group.Unbundled.Int
zpow_abs_eq_one : ∀ {G : Type u_1} [inst : Group G] (a : G) (n : ℤ), a ^ |n| = 1 ↔ a ^ n = 1
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.Bool.ite_then_ite'' : ∀ {α : Sort u_1} (c0 c1 : Bool) {a b : α}, (bif c0 then bif c1 then b else a else a) = bif c0 && c1 then b else a
-- Mathlib.Order.SuccPred.Basic
Order.le_of_lt_succ : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] {a b : α}, a < Order.succ b → a ≤ b
-- Mathlib.Topology.Order
generateFrom_insert_of_generateOpen : ∀ {α : Type u_1} {s : Set (Set α)} {t : Set α},
  TopologicalSpace.GenerateOpen s t → TopologicalSpace.generateFrom (insert t s) = TopologicalSpace.generateFrom s
-- Mathlib.Data.Rat.Lemmas
Rat.exists : ∀ {p : ℚ → Prop}, (∃ r, p r) ↔ ∃ a b, b ≠ 0 ∧ p (↑a / ↑b)
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.delete : {n : ℕ} →
  Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n →
    Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
NumberField.FinitePlace.hasFiniteMulSupport : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {x : K}, x ≠ 0 → Function.HasFiniteMulSupport fun w => w x
-- Mathlib.Algebra.Module.Presentation.Cokernel
Module.Presentation.cokernelSolution.isPresentation : ∀ {A : Type u} [inst : Ring A] {M₁ : Type v₁} {M₂ : Type v₂} [inst_1 : AddCommGroup M₁] [inst_2 : Module A M₁]
  [inst_3 : AddCommGroup M₂] [inst_4 : Module A M₂] (pres₂ : Module.Presentation A M₂) {f : M₁ →ₗ[A] M₂} {ι : Type w₁}
  {g₁ : ι → M₁} (data : pres₂.CokernelData f g₁),
  Submodule.span A (Set.range g₁) = ⊤ → (pres₂.cokernelSolution data).IsPresentation
-- Init.Core
/-- `HEq.ndrec` variant  -/
HEq.elim : {α : Sort u} → {a : α} → {p : α → Sort v} → {b : α} → a ≍ b → p a → p b
-- Mathlib.GroupTheory.Congruence.Defs
ConGen.Rel.refl : ∀ {M : Type u_1} [inst : Mul M] {r : M → M → Prop} (x : M), ConGen.Rel r x x
-- Mathlib.GroupTheory.Complement
/-- A right transversal can be viewed as a function mapping each element of the group
to the chosen representative from that right coset.  -/
AddSubgroup.IsComplement.toRightFun : {G : Type u_1} → [inst : AddGroup G] → {H : AddSubgroup G} → {T : Set G} → AddSubgroup.IsComplement (↑H) T → G → ↑T
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.lift_inr_inl : ∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : AddMonoid N],
  AddMonoid.Coprod.lift AddMonoid.Coprod.inr AddMonoid.Coprod.inl = AddMonoid.Coprod.swap M N
-- Mathlib.Algebra.Module.Presentation.Cokernel
/-- The cokernel can be defined by generators and relations.  -/
Module.Presentation.cokernelSolution.isPresentationCore : {A : Type u} →
  [inst : Ring A] →
    {M₁ : Type v₁} →
      {M₂ : Type v₂} →
        [inst_1 : AddCommGroup M₁] →
          [inst_2 : Module A M₁] →
            [inst_3 : AddCommGroup M₂] →
              [inst_4 : Module A M₂] →
                (pres₂ : Module.Presentation A M₂) →
                  {f : M₁ →ₗ[A] M₂} →
                    {ι : Type w₁} →
                      {g₁ : ι → M₁} →
                        (data : pres₂.CokernelData f g₁) →
                          Submodule.span A (Set.range g₁) = ⊤ → (pres₂.cokernelSolution data).IsPresentationCore
-- Mathlib.Topology.Sheaves.Stalks
/-- A version of `exists_germ_eq` that provides a section
over a subset of a given open neighborhood.  -/
TopCat.Presheaf.exists_le_germ_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  {FC : C → C → Type u_1} {CC : C → Type v} [inst_2 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
  [instCC : CategoryTheory.ConcreteCategory C FC]
  [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] (F : TopCat.Presheaf C X) {x : ↑X}
  (t : CategoryTheory.ToType (F.stalk x)) {V : TopologicalSpace.Opens ↑X},
  x ∈ V → ∃ U ≤ V, ∃ (m : x ∈ U), ∃ s, (CategoryTheory.ConcreteCategory.hom (F.germ U x m)) s = t
-- Mathlib.MeasureTheory.Integral.Indicator
/-- If the indicators of measurable sets `Aᵢ` tend pointwise almost everywhere to the indicator
of a measurable set `A` and we eventually have `Aᵢ ⊆ B` for some set `B` of finite measure, then
the measures of `Aᵢ` tend to the measure of `A`.  -/
MeasureTheory.tendsto_measure_of_ae_tendsto_indicator : ∀ {α : Type u_1} [inst : MeasurableSpace α] {A : Set α} {ι : Type u_2} (L : Filter ι) [L.IsCountablyGenerated]
  {As : ι → Set α} {μ : MeasureTheory.Measure α},
  MeasurableSet A →
    (∀ (i : ι), MeasurableSet (As i)) →
      ∀ {B : Set α},
        MeasurableSet B →
          μ B ≠ ⊤ →
            (∀ᶠ (i : ι) in L, As i ⊆ B) →
              (∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) → Filter.Tendsto (fun i => μ (As i)) L (nhds (μ A))
-- Batteries.Data.Vector.Basic
_private.Batteries.Data.Vector.Basic.0.Vector.scanlMFast : {m : Type u_1 → Type u_2} →
  {β : Type u_1} →
    {α : Type u_3} → {n : ℕ} → [Monad m] → (β → α → m β) → β → Vector α n → n < USize.size → m (Vector β (n + 1))
-- Init.Data.List.Scan.Lemmas
List.scanrM_eq_scanlM_reverse : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {init : β} {as : List α} [inst : Monad m] [LawfulMonad m]
  {f : α → β → m β}, List.scanrM f init as = List.reverse <$> List.scanlM (flip f) init as.reverse
-- Mathlib.Algebra.Lie.Normalizer
LieSubmodule.gc_top_lie_normalizer : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M],
  GaloisConnection (fun N => ⁅⊤, N⁆) LieSubmodule.normalizer
-- Mathlib.Order.WithBot
WithBot.lattice : {α : Type u_1} → [Lattice α] → Lattice (WithBot α)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.coboundariesToCocycles₂_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u_1, u, u} k G}
  (x : ↥(groupCohomology.coboundaries₂ A)), ⇑((groupCohomology.coboundariesToCocycles₂ A) x) = ↑x
-- Mathlib.Data.Fintype.Powerset
Finset.mem_powersetCard_univ : ∀ {α : Type u_1} [inst : Fintype α] {s : Finset α} {k : ℕ}, s ∈ Finset.powersetCard k Finset.univ ↔ s.card = k
-- Mathlib.Topology.Bornology.Basic
Bornology.ext_iff : ∀ {α : Type u_2} {t t' : Bornology α}, t = t' ↔ Bornology.cobounded α = Bornology.cobounded α
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_diff!_of_contains_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  m₁.WF → m₂.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k m₂ = true → (m₁.diff! m₂).get? k = none
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.instIsDomain : ∀ (R : Type u_1) [e : EuclideanDomain R], IsDomain R
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.natCast_kronecker : ∀ {α : Type u_3} {l : Type u_9} {m : Type u_10} {n : Type u_11} [inst : NonAssocSemiring α] [inst_1 : DecidableEq l]
  (a : ℕ) (B : Matrix m n α),
  Matrix.kroneckerMap (fun x1 x2 => x1 * x2) (↑a) B =
    (Matrix.reindex (Equiv.prodComm m l) (Equiv.prodComm n l)) (Matrix.blockDiagonal fun x => a • B)
-- Mathlib.Data.ENat.Lattice
ENat.add_iInf₂ : ∀ {ι : Sort u_2} {a : ℕ∞} {κ : ι → Sort u_4} (f : (i : ι) → κ i → ℕ∞), a + ⨅ i, ⨅ j, f i j = ⨅ i, ⨅ j, a + f i j
-- Mathlib.Order.Interval.Set.Defs
Set.mem_Ici : ∀ {α : Type u_1} [inst : Preorder α] {b x : α}, x ∈ Set.Ici b ↔ b ≤ x
-- Lean.Expr
Lean.Expr.letNondep! : Lean.Expr → Bool
-- Mathlib.Condensed.Light.Epi
LightCondensed.instEpiLightCondModMapNat : ∀ {R : Type u} [inst : Ring R] {M N : ℕ → LightCondMod R} (f : (n : ℕ) → M n ⟶ N n)
  [∀ (n : ℕ), CategoryTheory.Epi (f n)], CategoryTheory.Epi (CategoryTheory.Limits.Pi.map f)
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.ExprCnstr.mk : Bool → Nat.Internal.Linear.Expr → Nat.Internal.Linear.Expr → Nat.Internal.Linear.ExprCnstr
-- Init.Data.String.Lemmas.FindPos
String.posGE.congr_simp : ∀ (s : String) (offset offset_1 : String.Pos.Raw) (e_offset : offset = offset_1) (h : offset ≤ s.rawEndPos),
  s.posGE offset h = s.posGE offset_1 ⋯
-- Mathlib.Order.RelClasses
/-- The relation is `WellFounded`, as a proposition.  -/
IsWellFounded.wf : ∀ {α : Type u} {r : α → α → Prop} [self : IsWellFounded α r], WellFounded r
-- Mathlib.Algebra.Module.Torsion.Basic
AddSubgroup.torsionBy.nsmul : ∀ {A : Type u_3} [inst : AddCommGroup A] {n : ℕ} (x : ↥(AddSubgroup.torsionBy A ↑n)), n • x = 0
-- Mathlib.Geometry.Manifold.VectorField.Pullback
VectorField.mpullbackWithin.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] (I' : ModelWithCorners 𝕜 E' H')
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] (f : M → M')
  (V : (x : M') → TangentSpace I' x) (s : Set M) (x : M),
  VectorField.mpullbackWithin I I' f V s x = (mfderiv[s] f x).inverse (V (f x))
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.eq_symm_apply : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁]
  [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂]
  (e : P₁ ≃ᴬ[k] P₂) {x : P₂} {y : P₁}, y = e.symm x ↔ e y = x
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.Pos.skipWhile_bool_eq_self_iff_get : ∀ {p : Char → Bool} {s : String.Slice} {pos : s.Pos},
  pos.skipWhile p = pos ↔ ∀ (h : pos ≠ s.endPos), p (pos.get h) = false
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddSound
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddSound.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ofArray_fold_fn.match_3.eq_2 : ∀ {n : ℕ} (motive : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → Sort u_1)
  (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (h_1 : Unit → motive none)
  (h_2 : (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → motive (some c)),
  (match some c with
    | none => h_1 ()
    | some c => h_2 c) =
    h_2 c
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.indepFun_mul_mul₀ : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10}
  {m : MeasurableSpace β} [inst : Mul β] [MeasurableMul₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iIndepFun f μ →
    (∀ (i : ι), AEMeasurable (f i) μ) →
      ∀ (i j k l : ι), i ≠ k → i ≠ l → j ≠ k → j ≠ l → ProbabilityTheory.IndepFun (f i * f j) (f k * f l) μ
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_image_eq : ∀ {α β : Type u} {f : α → β} {s : Set α}, Function.Injective f → Cardinal.mk ↑(f '' s) = Cardinal.mk ↑s
-- Aesop.Tree.Data
Aesop.Goal.currentGoalAndMetaState : Aesop.Goal → Lean.Meta.SavedState → Lean.MetaM (Lean.MVarId × Lean.Meta.SavedState)
-- Mathlib.Order.CompleteLattice.Basic
Prop.instCompleteLinearOrder : CompleteLinearOrder Prop
-- Init.Data.Range.Polymorphic.Lemmas
Std.Ric.toList_succ_eq_map : ∀ {α : Type u} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [Std.PRange.LinearlyUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [inst_6 : Std.PRange.InfinitelyUpwardEnumerable α]
  [inst_7 : Std.Rxc.IsAlwaysFinite α] [inst_8 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_9 : Std.PRange.LawfulUpwardEnumerableLeast? α] {hi : α},
  (*...=Std.PRange.succ hi).toList = Std.PRange.UpwardEnumerable.least :: List.map Std.PRange.succ (*...=hi).toList
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion
SemiNormedGrp.completion_completeSpace : ∀ {V : SemiNormedGrp}, CompleteSpace (SemiNormedGrp.completion.obj V).carrier
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
Int.prime_absNorm : ∀ (J : Ideal ℤ), Nat.Prime (Ideal.absNorm J) ↔ Prime J
-- Mathlib.Data.Finset.SDiff
Finset.insert_sdiff_cancel : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {a : α}, a ∉ s → insert a s \ s = {a}
-- Mathlib.CategoryTheory.Action.Basic
Action.Hom.mk.sizeOf_spec : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] {M N : Action V G}
  [inst_2 : SizeOf V] [inst_3 : SizeOf G] (hom : M.V ⟶ N.V)
  (comm :
    autoParam
      (∀ (g : G), CategoryTheory.CategoryStruct.comp (M.ρ g) hom = CategoryTheory.CategoryStruct.comp hom (N.ρ g))
      Action.Hom.comm._autoParam),
  sizeOf { hom := hom, comm := comm } = 1 + sizeOf hom