mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mathlib.Tactic.MonTauto.mul_assoc_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M X : C}
  [inst_2 : CategoryTheory.MonObj M] (f : X ⟶ M),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X M M).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f CategoryTheory.MonObj.mul)
        CategoryTheory.MonObj.mul) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.CategoryStruct.id M))
          CategoryTheory.MonObj.mul)
        (CategoryTheory.CategoryStruct.id M))
      CategoryTheory.MonObj.mul
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.hom_ofHom : ∀ {M N : Type u} [inst : AddMonoid M] [inst_1 : AddMonoid N] (f : M →+ N), AddMonCat.Hom.hom (AddMonCat.ofHom f) = f
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.coe_fst' : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e : Bundle.Trivialization F proj) {x : Z}, proj x ∈ e.baseSet → (↑e x).1 = proj x
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue_eq_getEntry_snd : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {k : α}
  {h' : Std.Internal.List.containsKey k l = true},
  Std.Internal.List.getValue k l h' = (Std.Internal.List.getEntry k l h').snd
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
AbsoluteValue.eq_zero : ∀ {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  (abv : AbsoluteValue R S) {x : R}, abv x = 0 ↔ x = 0
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.monoidalCategory : {I : Type u} →
  [inst : AddMonoid I] →
    {C : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [∀ (X₁ X₂ : CategoryTheory.GradedObject I C), X₁.HasTensor X₂] →
            [∀ (X₁ X₂ X₃ : CategoryTheory.GradedObject I C), X₁.HasGoodTensor₁₂Tensor X₂ X₃] →
              [∀ (X₁ X₂ X₃ : CategoryTheory.GradedObject I C), X₁.HasGoodTensorTensor₂₃ X₂ X₃] →
                [DecidableEq I] →
                  [CategoryTheory.Limits.HasInitial C] →
                    [∀ (X₁ : C),
                          CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C)
                            ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁)] →
                      [∀ (X₂ : C),
                            CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C)
                              ((CategoryTheory.MonoidalCategory.curriedTensor C).flip.obj X₂)] →
                        [∀ (X₁ X₂ X₃ X₄ : CategoryTheory.GradedObject I C), X₁.HasTensor₄ObjExt X₂ X₃ X₄] →
                          CategoryTheory.MonoidalCategory (CategoryTheory.GradedObject I C)
-- Mathlib.Tactic.MoveAdd
/-- If `sum` is an expression consisting of repeated applications of `op`, then `getAddends`
returns the Array of those recursively determined arguments whose type is DefEq to `R`.  -/
Mathlib.MoveAdd.getAddends : Lean.Name → Lean.Expr → Lean.Expr → Lean.MetaM (Array Lean.Expr)
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
/-- If `G.IsBipartiteWith s t` and `w ∈ t`, then the neighbor set of `w` is disjoint to `t`.  -/
SimpleGraph.isBipartiteWith_neighborSet_disjoint' : ∀ {V : Type u_1} {w : V} {G : SimpleGraph V} {s t : Set V}, G.IsBipartiteWith s t → w ∈ t → Disjoint (G.neighborSet w) t
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.addCommGroup.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_4}
  [inst_5 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_6} [inst_7 : TopologicalSpace N] [inst_8 : ChartedSpace H N]
  {n : WithTop ℕ∞} {G : Type u_10} [inst_9 : AddCommGroup G] [inst_10 : TopologicalSpace G]
  [inst_11 : ChartedSpace H' G] [inst_12 : LieAddGroup I' n G],
  ContMDiffMap.addCommGroup = { toAddGroup := ContMDiffMap.addGroup, add_comm := ⋯ }
-- Lean.LibrarySuggestions.SymbolFrequency
/-- Return the number of times a `Name` appears
in the signatures of (non-internal) theorems in the imported environment,
skipping instance arguments and proofs.
 -/
Lean.LibrarySuggestions.symbolFrequency : Lean.Name → Lean.CoreM ℕ
-- Mathlib.Topology.Connected.Basic
/-- The closure of a preconnected set is preconnected as well.  -/
IsPreconnected.closure : ∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α}, IsPreconnected s → IsPreconnected (closure s)
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.below.mul_assoc : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  {motive : (a a_1 : RingCat.Colimits.Prequotient F) → RingCat.Colimits.Relation F a a_1 → Prop}
  (x y z : RingCat.Colimits.Prequotient F), RingCat.Colimits.Relation.below ⋯
-- Std.Async.System
/-- Gets the hostname of the machine.
 -/
Std.Async.System.getHostName : IO String
-- Mathlib.Computability.TuringMachine.Tape
Turing.ListBlank.map_cons : ∀ {Γ : Type u_1} {Γ' : Type u_2} [inst : Inhabited Γ] [inst_1 : Inhabited Γ'] (f : Turing.PointedMap Γ Γ')
  (l : Turing.ListBlank Γ) (a : Γ),
  Turing.ListBlank.map f (Turing.ListBlank.cons a l) = Turing.ListBlank.cons (f.f a) (Turing.ListBlank.map f l)
-- Init.Data.Array.Count
Array.countP_false : ∀ {α : Type u_1}, (Array.countP fun x => false) = Function.const (Array α) 0
-- Mathlib.Combinatorics.SimpleGraph.IncMatrix
SimpleGraph.incMatrix_mul_transpose : ∀ {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [inst : Fintype (Sym2 α)] [inst_1 : DecidableEq α]
  [inst_2 : DecidableRel G.Adj] [inst_3 : Semiring R] [inst_4 : G.LocallyFinite],
  SimpleGraph.incMatrix R G * (SimpleGraph.incMatrix R G).transpose =
    Matrix.of fun a b => if a = b then ↑(G.degree a) else if G.Adj a b then 1 else 0
-- Init.Data.Bool
Bool.cond_else_self : ∀ (c b : Bool), (bif c then b else c) = (c && b)
-- Mathlib.Algebra.Order.Monoid.Defs
IsOrderedCancelAddMonoid.toIsOrderedAddMonoid : ∀ {α : Type u_2} {inst : AddCommMonoid α} {inst_1 : Preorder α} [self : IsOrderedCancelAddMonoid α],
  IsOrderedAddMonoid α
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
quadraticChar_zero : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F], (quadraticChar F) 0 = 0
-- Mathlib.Data.Setoid.Partition
IndexedPartition.class_of : ∀ {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) {x : α},
  Set.ofPred (hs.setoid x) = s (hs.index x)
-- Init.Data.List.Count
List.count_erase : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a b : α} {l : List α},
  List.count a (l.erase b) = List.count a l - if (b == a) = true then 1 else 0
-- Mathlib.RingTheory.Coalgebra.Hom
/-- See Note [custom simps projection]  -/
CoalgHom.Simps.apply : {R : Type u_6} →
  {α : Type u_7} →
    {β : Type u_8} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid α] →
          [inst_2 : Module R α] →
            [inst_3 : AddCommMonoid β] →
              [inst_4 : Module R β] →
                [inst_5 : CoalgebraStruct R α] → [inst_6 : CoalgebraStruct R β] → (α →ₗc[R] β) → α → β
-- Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
/-- The restriction of an s-finite measure `μ` to `μ.sigmaFiniteSet` is sigma-finite.  -/
MeasureTheory.instSigmaFiniteRestrictSigmaFiniteSet : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α},
  MeasureTheory.SigmaFinite (μ.restrict μ.sigmaFiniteSet)
-- Mathlib.RingTheory.Extension.Cotangent.Free
Algebra.Generators.cotangentRestrict.congr_simp : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type w}
  (P : Algebra.Generators R S ι) {σ : Type u_1} {u u_1 : σ → ι} (e_u : u = u_1) (hu : Function.Injective u),
  P.cotangentRestrict hu = P.cotangentRestrict ⋯
-- Lean.Elab.Do.Legacy
/-- A `doMatchExpr` alternative.  -/
Lean.Elab.Term.Do.AltExpr : Type → Type
-- Mathlib.Algebra.Lie.Nilpotent
LieModule.IsFaithful.congr_simp : ∀ (R : Type u) (L : Type v) (M : Type w) [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],
  LieModule.IsFaithful R L M = LieModule.IsFaithful R L M
-- Mathlib.Topology.PartialHomeomorph.Basic
PartialHomeomorph.secondCountableTopology_source : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialHomeomorph X Y)
  [SecondCountableTopology Y], SecondCountableTopology ↑e.source
-- Mathlib.Analysis.Meromorphic.TrailingCoefficient
/-- If `f` is not meromorphic at `x`, the trailing coefficient is zero by definition.
 -/
meromorphicTrailingCoeffAt_of_not_MeromorphicAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜}, ¬MeromorphicAt f x → meromorphicTrailingCoeffAt f x = 0
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.instInhabitedRefinedDiscrTree : {a : Type} → Inhabited (Lean.Meta.RefinedDiscrTree a)
-- Mathlib.MeasureTheory.Measure.Content
/-- The measure induced by the outer measure coming from a content, on the Borel sigma-algebra.  -/
MeasureTheory.Content.measure : {G : Type w} →
  [inst : TopologicalSpace G] →
    MeasureTheory.Content G → [R1Space G] → [S : MeasurableSpace G] → [BorelSpace G] → MeasureTheory.Measure G
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
/-- Extension for the `positivity` tactic: `Real.sinh` is positive/nonnegative/nonzero if its input
is.  -/
Mathlib.Meta.Positivity.evalSinh : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.linear_prodCongr : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {P₃ : Type u_4} {P₄ : Type u_5} {V₁ : Type u_6} {V₂ : Type u_7}
  {V₃ : Type u_8} {V₄ : Type u_9} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂]
  [inst_3 : AddCommGroup V₃] [inst_4 : AddCommGroup V₄] [inst_5 : Module k V₁] [inst_6 : Module k V₂]
  [inst_7 : Module k V₃] [inst_8 : Module k V₄] [inst_9 : AddTorsor V₁ P₁] [inst_10 : AddTorsor V₂ P₂]
  [inst_11 : AddTorsor V₃ P₃] [inst_12 : AddTorsor V₄ P₄] (e₁ : P₁ ≃ᵃ[k] P₂) (e₂ : P₃ ≃ᵃ[k] P₄),
  (e₁.prodCongr e₂).linear = e₁.linear.prodCongr e₂.linear
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
/-- `a ^ x` bundled as an element of `Aˣ` for `a : Aˣ`.  -/
Units.cfcRpow : {A : Type u_1} →
  [inst : PartialOrder A] →
    [inst_1 : Ring A] →
      [inst_2 : StarRing A] →
        [inst_3 : TopologicalSpace A] →
          [StarOrderedRing A] →
            [inst_5 : Algebra ℝ A] →
              [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] →
                [NonnegSpectrumClass ℝ A] → (a : Aˣ) → ℝ → autoParam (0 ≤ ↑a) Units.cfcRpow._auto_1 → Aˣ
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.subst_into_add : ∀ {α : Type u_1} [inst : AddCommMonoid α] (l r tl tr t : α), l = tl → r = tr → tl + tr = t → l + r = t
-- Init.Data.Int.Order
Int.sub_lt_sub_of_lt_of_le : ∀ {a b c d : ℤ}, a < b → c ≤ d → a - d < b - c
-- Mathlib.GroupTheory.Perm.Fin
Equiv.Perm.decomposeFin_symm_apply_zero : ∀ {n : ℕ} (p : Fin (n + 1)) (e : Equiv.Perm (Fin n)), (Equiv.Perm.decomposeFin.symm (p, e)) 0 = p
-- Mathlib.Analysis.Calculus.ContDiff.Operations
ContDiff.pow : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {n : WithTop ℕ∞} {𝔸 : Type u_3} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸]
  {f : E → 𝔸}, ContDiff 𝕜 n f → ∀ (m : ℕ), ContDiff 𝕜 n fun x => f x ^ m
-- Mathlib.RingTheory.Artinian.Module
isArtinian_of_quotient_of_artinian : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (N : Submodule R M)
  [IsArtinian R M], IsArtinian R (M ⧸ N)
-- Mathlib.Algebra.Category.Semigrp.Basic
MagmaCat.hom_inv_apply : ∀ {M N : MagmaCat} (e : M ≅ N) (s : ↑N),
  (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s
-- Lean.Meta.Tactic.Grind.Arith.Util
Lean.Meta.Grind.Arith.CollectDecVars.State.mk.injEq : ∀ (visited : Std.HashSet UInt64) (found : Lean.FVarIdSet) (visited_1 : Std.HashSet UInt64) (found_1 : Lean.FVarIdSet),
  ({ visited := visited, found := found } = { visited := visited_1, found := found_1 }) =
    (visited = visited_1 ∧ found = found_1)
-- Mathlib.Algebra.Module.LocalizedModule.Int
IsLocalizedModule.finsetIntegerMultiple_image : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] {M' : Type u_3} [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  [inst_5 : IsLocalizedModule S f] [inst_6 : DecidableEq M] (s : Finset M'),
  ⇑f '' ↑(IsLocalizedModule.finsetIntegerMultiple S f s) = IsLocalizedModule.commonDenomOfFinset S f s • ↑s
-- Init.Data.Array.Lemmas
Array.instDecidableMemOfLawfulBEq : {α : Type u_1} → [inst : BEq α] → [LawfulBEq α] → (a : α) → (as : Array α) → Decidable (a ∈ as)
-- Init.Data.UInt.Bitwise
UInt16.ofFin_shiftRight_mod : ∀ (a b : Fin UInt16.size), UInt16.ofFin (a >>> (b % 16)) = UInt16.ofFin a >>> UInt16.ofFin b
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.mem_carrier : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {s : Subalgebra R A}
  {x : A}, x ∈ s.carrier ↔ x ∈ s
-- Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
AlgebraicGeometry.IsSchemeTheoreticallyDominant.mk : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  AlgebraicGeometry.Scheme.Hom.ker f = ⊥ → AlgebraicGeometry.IsSchemeTheoreticallyDominant f
-- Init.Data.Range.Polymorphic.SInt
Int8.instRxoIsAlwaysFinite : Std.Rxo.IsAlwaysFinite Int8
-- Mathlib.Algebra.Group.Units.Defs
/-- Units of an `AddMonoid`, bundled version.

An element of an `AddMonoid` is a unit if it has a two-sided additive inverse.
This version bundles the inverse element so that it can be computed.
For a predicate see `isAddUnit`.  -/
AddUnits : (α : Type u) → [AddMonoid α] → Type u
-- Init.Data.List.Lemmas
List.all_eq_false : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, l.all p = false ↔ ∃ x ∈ l, ¬p x = true
-- Init.Prelude
/-- Implementation of `mkMethods`.  -/
Lean.Macro.mkMethodsImp : Lean.Macro.Methods → Lean.Macro.MethodsRef
-- Lean.Meta.RecursorInfo
Lean.Meta.RecursorInfo.numMinors : Lean.Meta.RecursorInfo → ℕ
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
/-- One can reformulate smoothness as continuity and smoothness in any extended chart in the
target.  -/
mdifferentiable_iff_target : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} [IsManifold I 1 M]
  [IsManifold I' 1 M'],
  MDiff f ↔ Continuous f ∧ ∀ (y : M'), MDiff[f ⁻¹' (extChartAt I' y).source] (↑(extChartAt I' y) ∘ f)
-- Mathlib.Combinatorics.SimpleGraph.Copy
_private.Mathlib.Combinatorics.SimpleGraph.Copy.0.SimpleGraph.killCopies_of_ne_bot : ∀ {V : Type u_1} {W : Type u_2} {H : SimpleGraph W} (hH : H ≠ ⊥) (G : SimpleGraph V),
  G.killCopies H = G.deleteEdges (⋃ G', ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some})
-- Init.Grind.ToIntLemmas
Lean.Grind.ToInt.neg_congr : ∀ {α : Type u_1} {i : Lean.Grind.IntInterval} [inst : Lean.Grind.ToInt α i] [inst_1 : Neg α] [Lean.Grind.ToInt.Neg α i]
  {a : α} {a' : ℤ}, ↑a = a' → ↑(-a) = i.wrap (-a')
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.real_toNNReal : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  MeasureTheory.Integrable f μ → MeasureTheory.Integrable (fun x => ↑(f x).toNNReal) μ
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.PolyCnstr.mk.injEq : ∀ (eq : Bool) (lhs rhs : Nat.Internal.Linear.Poly) (eq_1 : Bool) (lhs_1 rhs_1 : Nat.Internal.Linear.Poly),
  ({ eq := eq, lhs := lhs, rhs := rhs } = { eq := eq_1, lhs := lhs_1, rhs := rhs_1 }) =
    (eq = eq_1 ∧ lhs = lhs_1 ∧ rhs = rhs_1)
-- Lean.Meta.Tactic.Simp.Arith.Int.Basic
Lean.Meta.Simp.Arith.Int.ToLinear.eqCnstr? : Lean.Expr → Lean.Meta.Simp.Arith.Int.ToLinear.M (Option (Int.Internal.Linear.Expr × Int.Internal.Linear.Expr))
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.addCommute_iff : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → Add (f i)] {x y : (i : I) → f i},
  AddCommute x y ↔ ∀ (i : I), AddCommute (x i) (y i)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.IsReduced.append_overlap : ∀ {α : Type u} {L₁ L₂ L₃ : List (α × Bool)},
  FreeGroup.IsReduced (L₁ ++ L₂) → FreeGroup.IsReduced (L₂ ++ L₃) → L₂ ≠ [] → FreeGroup.IsReduced (L₁ ++ L₂ ++ L₃)
-- Mathlib.AlgebraicTopology.SimplexCategory.Defs
/-- Constructor `ℕ → SimplexCategory`.  -/
SimplexCategory.mk : ℕ → SimplexCategory
-- Mathlib.Data.EReal.Inv
EReal.coe_ennreal_pow : ∀ (x : ENNReal) (n : ℕ), ↑(x ^ n) = ↑x ^ n
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.subset_iUnion : ∀ {α : Type u_1} [inst : Small.{u, u_1} α] (f : α → ZFSet.{u}) (i : α), f i ⊆ ZFSet.iUnion fun i => f i
-- Init.Grind.Norm
Lean.Grind.exists_and_right : ∀ {α : Sort u} {p : α → Prop} {b : Prop}, (∃ x, p x ∧ b) = ((∃ x, p x) ∧ b)
-- Mathlib.Topology.Connected.Basic
/-- If a preconnected set `s` intersects an open set `u`, and limit points of `u` inside `s` are
contained in `u`, then the whole set `s` is contained in `u`.  -/
IsPreconnected.subset_of_closure_inter_subset : ∀ {α : Type u} [inst : TopologicalSpace α] {s u : Set α},
  IsPreconnected s → IsOpen u → (s ∩ u).Nonempty → closure u ∩ s ⊆ u → s ⊆ u
-- Mathlib.Analysis.Calculus.FDeriv.Prod
hasFDerivWithinAt_pi : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {s : Set E} {ι : Type u_6} {F' : ι → Type u_7}
  [inst_3 : (i : ι) → NormedAddCommGroup (F' i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (F' i)] {φ : (i : ι) → E → F' i}
  {φ' : (i : ι) → E →L[𝕜] F' i},
  HasFDerivWithinAt (fun x i => φ i x) (ContinuousLinearMap.pi φ') s x ↔ ∀ (i : ι), HasFDerivWithinAt (φ i) (φ' i) s x
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.zero_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (x : α) [inst_2 : Zero β],
  0 x = 0
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.add.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) {T : C}
  (f : T ⟶ S), E.add f = (E.sum (CategoryTheory.PreZeroHypercover.singleton f)).reindex (Equiv.optionEquivSumPUnit E.I₀)
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
/-- A basis of the quotient `(𝓞 K)ˣ ⧸ (torsion K)` seen as an additive ℤ-module.  -/
NumberField.Units.basisModTorsion : (K : Type u_1) →
  [inst : Field K] →
    [inst_1 : NumberField K] →
      Module.Basis (Fin (NumberField.Units.rank K)) ℤ
        (Additive ((NumberField.RingOfIntegers K)ˣ ⧸ NumberField.Units.torsion K))
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
AlgebraicGeometry.Scheme.exists_isOpenCover_and_isAffine_of_finite : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme)
  (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [CategoryTheory.IsCofiltered I]
  [∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)] [∀ (i : I), CompactSpace ↥(D.obj i)]
  [∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)] {J : Type u_1} [Finite J] (U : J → c.pt.Opens),
  TopologicalSpace.IsOpenCover U →
    (∀ (i : J), AlgebraicGeometry.IsAffineOpen (U i)) →
      ∃ i V,
        TopologicalSpace.IsOpenCover V ∧
          ∀ (j : J),
            AlgebraicGeometry.IsAffineOpen (V j) ∧ U j = (TopologicalSpace.Opens.map (c.π.app i).base).obj (V j)
-- Mathlib.Algebra.Group.TypeTags.Hom
MonoidHom.coe_toAdditive : ∀ {α : Type u_3} {β : Type u_4} [inst : MulOneClass α] [inst_1 : MulOneClass β] (f : α →* β),
  ⇑(MonoidHom.toAdditive f) = ⇑Additive.ofMul ∘ ⇑f ∘ ⇑Additive.toMul
-- Batteries.Recycling.RBTree.Basic
/-- `O(log n)`. Insert element `v` into the tree.  -/
RBTree.RBSet.insert : {α : Type u_1} → {cmp : α → α → Ordering} → RBTree.RBSet α cmp → α → RBTree.RBSet α cmp
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.exactly.go : {α : Type} → Std.Internal.Parsec.String.Parser α → ℕ → Array α → ℕ → Std.Internal.Parsec.String.Parser (Array α)
-- Mathlib.Data.ENNReal.Operations
ENNReal.le_sub_iff_add_le_right : ∀ {a b c : ENNReal}, c ≠ ⊤ → c ≤ b → (a ≤ b - c ↔ a + c ≤ b)
-- Mathlib.Algebra.Ring.GrindInstances
Ring.toGrindRing : (α : Type u_1) → [s : Ring α] → Lean.Grind.Ring α
-- Mathlib.Algebra.MonoidAlgebra.Module
MonoidAlgebra.mapDomain_smul : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Monoid S] [inst_1 : Semiring R]
  [inst_2 : DistribMulAction S R] (f : M → N) (s : S) (x : MonoidAlgebra R M),
  MonoidAlgebra.mapDomain f (s • x) = s • MonoidAlgebra.mapDomain f x
-- Mathlib.Algebra.Group.Action.Pi
Function.extend_vadd : ∀ {ι : Type u_1} {M : Type u_7} {α : Type u_8} {β : Type u_9} [inst : VAdd M β] (r : M) (f : ι → α) (g : ι → β)
  (e : α → β), Function.extend f (r +ᵥ g) (r +ᵥ e) = r +ᵥ Function.extend f g e
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.baseChange_polynomialX : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Jacobian R) {S : Type s} [inst_1 : CommRing S] {A : Type u}
  [inst_2 : CommRing A] {B : Type v} [inst_3 : CommRing B] [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  (f : A →ₐ[S] B), (W'.baseChange B).polynomialX = (MvPolynomial.map ↑f) (W'.baseChange A).polynomialX
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
isBigO_deriv_ofReal_cpow_const_atTop : ∀ (c : ℂ), (deriv fun x => ↑x ^ c) =O[Filter.atTop] fun x => x ^ (c.re - 1)
-- Std.Async.TCP
/-- Receives data from the client socket. If data is received, it’s wrapped in .some. If EOF is reached,
the result is .none, indicating no more data is available. Receiving data in parallel on the same
socket is not supported. Instead, we recommend binding multiple sockets to the same address.
Furthermore calling this function in parallel with `recvSelector` is not supported.
 -/
Std.Async.TCP.Socket.Client.recv? : Std.Async.TCP.Socket.Client → UInt64 → Std.Async.Async (Option ByteArray)
-- Mathlib.Data.Fin.SuccPred
/-- `succ` commutes with `predAbove`.  -/
Fin.succ_predAbove_succ : ∀ {n : ℕ} (a : Fin n) (b : Fin (n + 1)), a.succ.predAbove b.succ = (a.predAbove b).succ
-- Mathlib.CategoryTheory.Limits.Connected
CategoryTheory.ProdPreservesConnectedLimits.γ₂_app : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] [inst_1 : CategoryTheory.Limits.HasBinaryProducts C]
  {J : Type v₂} [inst_2 : CategoryTheory.SmallCategory J] {K : CategoryTheory.Functor J C} (X : C) (x : J),
  (CategoryTheory.ProdPreservesConnectedLimits.γ₂ X).app x = CategoryTheory.Limits.prod.snd
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get?_eq_none_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {a : α}, t.contains a = false → t.get? a = none
-- Mathlib.Algebra.Group.Int.Even
Int.emod_two_ne_zero : ∀ {n : ℤ}, ¬n % 2 = 0 ↔ n % 2 = 1