mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
AlgebraicIndependent.matroid_spanning_iff_of_subsingleton : ∀ {R : Type u_1} {A : Type w} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : FaithfulSMul R A] [inst_4 : Subsingleton A] {s : Set A},
  (AlgebraicIndependent.matroid R A).Spanning s ↔ s = Set.univ
-- Mathlib.Topology.Algebra.Support
isClosed_mulTSupport : ∀ {X : Type u_1} {α : Type u_2} [inst : One α] [inst_1 : TopologicalSpace X] (f : X → α), IsClosed (mulTSupport f)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
CategoryTheory.Limits.instIsIsoCoequalizerComparison : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {X Y : C} (f g : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasCoequalizer f g]
  [inst_3 : CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)]
  [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G],
  CategoryTheory.IsIso (CategoryTheory.Limits.coequalizerComparison f g G)
-- Mathlib.Algebra.BigOperators.Finprod
/-- To prove a property of a finite sum, it suffices to prove that the property is
additive and holds on the summands.  -/
finsum_induction : ∀ {M : Type u_2} {α : Sort u_4} [inst : AddCommMonoid M] {f : α → M} (p : M → Prop),
  p 0 → (∀ (x y : M), p x → p y → p (x + y)) → (∀ (i : α), p (f i)) → p (∑ᶠ (i : α), f i)
-- Mathlib.RingTheory.Perfection
Perfection.coeff_add_ne_zero : ∀ {R : Type u_1} [inst : CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [inst_1 : CharP R p] {f : Perfection R p}
  {n : ℕ}, (Perfection.coeff R p n) f ≠ 0 → ∀ (k : ℕ), (Perfection.coeff R p (n + k)) f ≠ 0
-- Mathlib.Order.Interval.Finset.Defs
Set.instFintypeIio : {α : Type u_1} → [inst : Preorder α] → [LocallyFiniteOrderBot α] → (a : α) → Fintype ↑(Set.Iio a)
-- Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Dynamics.netEntropyInfEntourage_empty : ∀ {X : Type u_1} {T : X → X} {U : SetRel X X}, Dynamics.netEntropyInfEntourage T ∅ U = ⊥
-- Mathlib.GroupTheory.DedekindFinite
instIsDedekindFiniteMonoidOfFinite : ∀ (M : Type u_1) [inst : Monoid M] [Finite M], IsDedekindFiniteMonoid M
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.combine.inj : ∀ {c₁ c₂ c₁_1 c₂_1 : Lean.Meta.Grind.Arith.Linear.IneqCnstr},
  Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.combine c₁ c₂ =
      Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.combine c₁_1 c₂_1 →
    c₁ = c₁_1 ∧ c₂ = c₂_1
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getD_insertMany_emptyWithCapacity_list_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k k' : α},
  (k == k') = true →
    ∀ {v fallback : β},
      List.Pairwise (fun a b => (a.1 == b.1) = false) l →
        (k, v) ∈ l →
          Std.DHashMap.Internal.Raw₀.Const.getD
              (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)) k'
              fallback =
            v
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.comap_id : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] (S : StarSubalgebra R A),
  StarSubalgebra.comap (StarAlgHom.id R A) S = S
-- Mathlib.Algebra.Homology.Embedding.Connect
_private.Mathlib.Algebra.Homology.Embedding.Connect.0.CochainComplex.ConnectData.X.match_1.splitter : (motive : ℤ → Sort u_1) → (x : ℤ) → ((n : ℕ) → motive (Int.ofNat n)) → ((n : ℕ) → motive (Int.negSucc n)) → motive x
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
/-- If `f : R → ℝ` is a nonnegative, multiplicatively bounded function, then
`seminormFromBounded' f` is submultiplicative.  -/
seminormFromBounded_mul : ∀ {R : Type u_1} [inst : CommRing R] {f : R → ℝ} {c : ℝ},
  0 ≤ f →
    (∀ (x y : R), f (x * y) ≤ c * f x * f y) →
      ∀ (x y : R), seminormFromBounded' f (x * y) ≤ seminormFromBounded' f x * seminormFromBounded' f y
-- Mathlib.RepresentationTheory.Homological.Resolution
_private.Mathlib.RepresentationTheory.Homological.Resolution.0.«termGⁿ» : Lean.ParserDescr
-- Mathlib.Analysis.Complex.Basic
AlgHom.mk'.congr_simp : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f f_1 : A →+* B) (e_f : f = f_1)
  (h : ∀ (c : R) (x : A), f (c • x) = c • f x), AlgHom.mk' f h = AlgHom.mk' f_1 ⋯
-- Mathlib.Order.Bounds.Image
IsLeast.isGreatest_image2 : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {f : α → β → γ}
  {s : Set α} {t : Set β} {a : α} {b : β},
  (∀ (b : β), Antitone (Function.swap f b)) →
    (∀ (a : α), Antitone (f a)) → IsLeast s a → IsLeast t b → IsGreatest (Set.image2 f s t) (f a b)
-- Mathlib.Data.Finset.Fold
Finset.fold_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op]
  {f : α → β} {b : β} {g : γ ↪ α} {s : Finset γ}, Finset.fold op b f (Finset.map g s) = Finset.fold op b (f ∘ ⇑g) s
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.deleteVerts_le : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {s : Set V}, G'.deleteVerts s ≤ G'
-- Mathlib.LinearAlgebra.RootSystem.Chain
RootPairing.chainTopCoeff_sub_chainBotCoeff : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : CharZero R] [inst_3 : IsDomain R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsCrystallographic] {i j : ι},
  LinearIndependent R ![P.root i, P.root j] →
    ↑(RootPairing.chainTopCoeff i j) - ↑(RootPairing.chainBotCoeff i j) = -P.pairingIn ℤ j i
-- Init.Data.Array.Range
Array.mem_zipIdx : ∀ {α : Type u_1} {x : α} {i : ℕ} {xs : Array α} {k : ℕ} (h : (x, i) ∈ xs.zipIdx k),
  k ≤ i ∧ i < k + xs.size ∧ x = xs[i - k]
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
/-- the natural transformations between the left components  -/
CategoryTheory.Limits.CatCospanTransformMorphism.left : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      {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} →
                      [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'} →
                                {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} →
                                  CategoryTheory.Limits.CatCospanTransformMorphism ψ ψ' → (ψ.left ⟶ ψ'.left)
-- Init.Data.String.PosRaw
String.Pos.Raw.inc_le : ∀ {p q : String.Pos.Raw}, p.inc ≤ q ↔ p < q
-- Mathlib.Algebra.Homology.ShortComplex.QuasiIso
CategoryTheory.ShortComplex.quasiIso_iff_isIso_rightHomologyMap' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology] (φ : S₁ ⟶ S₂)
  (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData),
  CategoryTheory.ShortComplex.QuasiIso φ ↔ CategoryTheory.IsIso (CategoryTheory.ShortComplex.rightHomologyMap' φ h₁ h₂)
-- Mathlib.GroupTheory.GroupAction.Hom
DistribMulActionHom.zero_apply : ∀ {M : Type u_1} [inst : Monoid M] {A : Type u_4} [inst_1 : AddMonoid A] [inst_2 : DistribMulAction M A] (a : A),
  1 a = a
-- Mathlib.Algebra.Order.Archimedean.Basic
existsUnique_zsmul_near_of_pos' : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] {a : G},
  0 < a → ∀ (g : G), ∃! k, 0 ≤ g - k • a ∧ g - k • a < a
-- Mathlib.Algebra.GCDMonoid.Basic
gcd_eq_left_iff : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (a b : α),
  normalize a = a → (gcd a b = a ↔ a ∣ b)
-- Std.Internal.UV.System
Std.Internal.UV.System.instReprCPUInfo : Repr Std.Internal.UV.System.CPUInfo
-- Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
/-- The associated precoverage to a pre-`0`-hypercover family.  -/
CategoryTheory.PreZeroHypercoverFamily.precoverage : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.PreZeroHypercoverFamily C → CategoryTheory.Precoverage C
-- Mathlib.RingTheory.DedekindDomain.Factorization
Associates.finprod_ne_zero : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (I : Ideal R),
  Associates.mk (∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R), v.maxPowDividing I) ≠ 0
-- Mathlib.RingTheory.Bialgebra.TensorProduct
Bialgebra.comm_comp_comulBialgHom : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A]
  [inst_3 : Coalgebra.IsCocomm R A],
  (Bialgebra.TensorProduct.comm R A A).toBialgHom.comp (Bialgebra.comulBialgHom R A) = Bialgebra.comulBialgHom R A
-- Mathlib.Order.Bounded
Set.bounded_ge_Icc : ∀ {α : Type u_1} [inst : Preorder α] (a b : α), Set.Bounded (fun x1 x2 => x1 ≥ x2) (Set.Icc a b)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
/-- The alphabet of the TM2 simulator on TM1 is a marker for the stack bottom,
plus a vector of stack elements for each stack, or none if the stack does not extend this far.  -/
Turing.TM2to1.Γ' : (K : Type u_1) → (K → Type u_2) → Type (max 0 u_1 u_2)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.adjoin_simple_eq_bot_iff : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {α : E}, F⟮α⟯ = ⊥ ↔ α ∈ ⊥
-- Mathlib.Algebra.Ring.Subsemiring.Defs
/-- `SubsemiringClass S R` states that `S` is a type of subsets `s ⊆ R` that
are both a multiplicative and an additive submonoid.  -/
SubsemiringClass : (S : Type u_1) → (R : outParam (Type u)) → [NonAssocSemiring R] → [SetLike S R] → Prop
-- Mathlib.Data.PNat.Defs
/-- Convert a natural number to a `PNat`. `n+1` is mapped to itself,
and `0` becomes `1`.  -/
Nat.toPNat' : ℕ → ℕ+
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.RegularEpi.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {X Y : C} {f : X ⟶ Y} {W : C} {left right : W ⟶ X}
  {w :
    autoParam (CategoryTheory.CategoryStruct.comp left f = CategoryTheory.CategoryStruct.comp right f)
      CategoryTheory.RegularEpi.w._autoParam}
  {isColimit : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ f w)} {W_1 : C}
  {left_1 right_1 : W_1 ⟶ X}
  {w_1 :
    autoParam (CategoryTheory.CategoryStruct.comp left_1 f = CategoryTheory.CategoryStruct.comp right_1 f)
      CategoryTheory.RegularEpi.w._autoParam}
  {isColimit_1 : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ f w_1)},
  { W := W, left := left, right := right, w := w, isColimit := isColimit } =
      { W := W_1, left := left_1, right := right_1, w := w_1, isColimit := isColimit_1 } →
    W = W_1 ∧ left ≍ left_1 ∧ right ≍ right_1 ∧ isColimit ≍ isColimit_1
-- Mathlib.Data.List.Nodup
List.nodup_iff_sublist : ∀ {α : Type u} {l : List α}, l.Nodup ↔ ∀ (a : α), ¬[a, a].Sublist l
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.mk₁_eqToHom_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X₀' X₀ X₁ : C} (h : X₀' = X₀) (f : X₀ ⟶ X₁),
  CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h) f) =
    CategoryTheory.ComposableArrows.mk₁ f
-- Mathlib.Algebra.Lie.IdealOperations
LieSubmodule.lie_sup : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N N' : LieSubmodule R L M) [inst_5 : LieAlgebra R L]
  (I : LieIdeal R L), ⁅I, N ⊔ N'⁆ = ⁅I, N⁆ ⊔ ⁅I, N'⁆
-- Std.Data.TreeSet.Raw.Basic
Std.TreeSet.Raw.instLawfulSingleton : ∀ {α : Type u} {cmp : α → α → Ordering}, LawfulSingleton α (Std.TreeSet.Raw α cmp)
-- Batteries.Data.Stream
Std.Stream.drop.eq_1 : ∀ {σ : Type u_1} {α : Type u_2} [inst : Std.Stream σ α] (s : σ), Std.Stream.drop s 0 = s
-- Std.Data.HashMap.Lemmas
Std.HashMap.isEmpty_inter_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  m₁.isEmpty = true → (m₁ ∩ m₂).isEmpty = true
-- Mathlib.Analysis.CStarAlgebra.GelfandDuality
IsStarNormal.nnnorm_add_eq_max : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] {a b : A},
  IsStarNormal a → IsStarNormal b → Commute a b → a * b = 0 → ‖a + b‖₊ = max ‖a‖₊ ‖b‖₊
-- Init.Data.Array.Lemmas
Array.getElem?_append : ∀ {α : Type u_1} {xs ys : Array α} {i : ℕ}, (xs ++ ys)[i]? = if i < xs.size then xs[i]? else ys[i - xs.size]?
-- Init.Notation
/-- `a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. -/
«term_+_» : Lean.TrailingParserDescr
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey_unitOfList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a == b) = false) l →
      k ∈ l → ∀ {h : k' ∈ Std.HashMap.unitOfList l}, (Std.HashMap.unitOfList l).getKey k' h = k
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
SSet.horn₂₀.sq : (SSet.stdSimplex.face {0}).BicartSq (SSet.stdSimplex.face {0, 1}) (SSet.stdSimplex.face {0, 2}) (SSet.horn 2 0)
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddSubsemigroup.ofClass.eq_1 : ∀ {S : Type u_3} {M : Type u_4} [inst : Add M] [inst_1 : SetLike S M] [inst_2 : AddMemClass S M] (s : S),
  AddSubsemigroup.ofClass s = { carrier := ↑s, add_mem' := ⋯ }
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.ofLEMk.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A : C} (X : CategoryTheory.Subobject B) (f f_1 : A ⟶ B)
  (e_f : f = f_1) [inst_1 : CategoryTheory.Mono f] (h : X ≤ CategoryTheory.Subobject.mk f),
  X.ofLEMk f h = X.ofLEMk f_1 ⋯
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData_left_H : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  [inst_3 : X.HasSpectralSequence data] (r r' : ℤ) (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq pq' pq'' : κ)
  (hpq : (c r).prev pq' = pq) (hpq' : (c r).next pq' = pq'') (i₀' i₀ i₁ i₂ i₃ i₃' : ι) (hi₀' : i₀' = data.i₀ r' pq' ⋯)
  (hi₀ : i₀ = data.i₀ r pq' ⋯) (hi₁ : i₁ = data.i₁ pq') (hi₂ : i₂ = data.i₂ pq') (hi₃ : i₃ = data.i₃ r pq' ⋯)
  (hi₃' : i₃' = data.i₃ r' pq' ⋯) (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq')
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData._auto_3),
  (X.spectralSequenceHomologyData data r r' hrr' hr pq pq' pq'' hpq hpq' i₀' i₀ i₁ i₂ i₃ i₃' hi₀' hi₀ hi₁ hi₂ hi₃ hi₃'
          n₀ n₁ n₂ hn₁' hn₁ hn₂).left.H =
    X.E (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
/-- The pointwise scalar addition of sets `s +ᵥ t` is defined as `{x +ᵥ y | x ∈ s, y ∈ t}` in locale
`Pointwise`.  -/
Set.vadd : {α : Type u_2} → {β : Type u_3} → [VAdd α β] → VAdd (Set α) (Set β)
-- Mathlib.Topology.ContinuousMap.Units
ContinuousMap.addUnitsLift_apply_neg_apply : ∀ {X : Type u_1} {M : Type u_2} [inst : TopologicalSpace X] [inst_1 : AddMonoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : ContinuousAdd M] (f : C(X, AddUnits M)) (x : X), ↑(-ContinuousMap.addUnitsLift f) x = ↑(-f x)
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubAddAction.ofFixingAddSubgroup.append_right : ∀ {M : Type u_1} {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] {s : Set α} {n : ℕ} [inst_2 : Finite ↑s]
  (x : Fin n ↪ ↥(SubAddAction.ofFixingAddSubgroup M s)) (i : Fin n),
  (SubAddAction.ofFixingAddSubgroup.append x) (Fin.natAdd s.ncard i) = ↑(x i)
-- Mathlib.Order.Category.FinBoolAlg
finBoolAlg_dual_comp_forget_to_finBddDistLat : FinBoolAlg.dual.comp (CategoryTheory.forget₂ FinBoolAlg FinBddDistLat) =
  (CategoryTheory.forget₂ FinBoolAlg FinBddDistLat).comp FinBddDistLat.dual
-- Mathlib.Algebra.Free
FreeMagma.instInhabited.eq_1 : ∀ {α : Type u} [inst : Inhabited α], FreeMagma.instInhabited = { default := FreeMagma.of default }
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
AddMonCat.FilteredColimits.colimitDesc.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCat)
  [inst_1 : CategoryTheory.IsFiltered J] (t : CategoryTheory.Limits.Cocone F),
  AddMonCat.FilteredColimits.colimitDesc F t =
    AddMonCat.ofHom
      {
        toFun :=
          (F.comp (CategoryTheory.forget AddMonCat)).descColimitType
            ((F.comp (CategoryTheory.forget AddMonCat)).coconeTypesEquiv.symm
              ((CategoryTheory.forget AddMonCat).mapCocone t)),
        map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Pi.comapEvalIsoEval_inv_app : ∀ {I : Type w₀} (C : I → Type u₁) [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₁} (h : J → I)
  (j : J) (X : (i : I) → C i),
  (CategoryTheory.Pi.comapEvalIsoEval C h j).inv.app X = CategoryTheory.CategoryStruct.id (X (h j))
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.natCast_def : ∀ {R : Type uR} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : AddCommMonoidWithOne A]
  [inst_2 : Module R A] [inst_3 : AddCommMonoidWithOne B] [inst_4 : Module R B] (n : ℕ), ↑n = ↑n ⊗ₜ[R] 1
-- Mathlib.Algebra.Category.Grp.Limits
/-- We show that the forgetful functor `AddGrpCat ⥤ AddMonCat` creates limits.

All we need to do is notice that the limit point has an `AddGroup` instance available, and then
reuse the existing limit.  -/
AddGrpCat.Forget₂.createsLimit : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J AddGrpCat) →
      CategoryTheory.CreatesLimit F (CategoryTheory.forget₂ AddGrpCat AddMonCat)
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.cardFactors_apply_prime_pow : ∀ {p k : ℕ}, Nat.Prime p → ArithmeticFunction.cardFactors (p ^ k) = k
-- Mathlib.Probability.Kernel.Composition.CompProd
/-- If `η` is a Markov kernel, use instead `fst_compProd` to get `(κ ⊗ₖ η).fst = κ`.  -/
ProbabilityTheory.Kernel.fst_compProd_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel (α × β) γ)
  [ProbabilityTheory.IsSFiniteKernel κ] [ProbabilityTheory.IsSFiniteKernel η] (x : α) {s : Set β},
  MeasurableSet s → ((κ.compProd η).fst x) s = ∫⁻ (b : β), s.indicator (fun b => (η (x, b)) Set.univ) b ∂κ x
-- Mathlib.Analysis.Normed.Group.Quotient
/-- The quotient in the category of normed groups.  -/
QuotientGroup.instNormedCommGroup : {M : Type u_1} → [inst : SeminormedCommGroup M] → (S : Subgroup M) → [hS : IsClosed ↑S] → NormedCommGroup (M ⧸ S)
-- Aesop.Tracing
Aesop.ruleFailureEmoji : String
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.instSMulCommClassSubtypeMemTorsion' : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (S : Type u_3)
  [inst_3 : CommMonoid S] [inst_4 : DistribMulAction S M] [inst_5 : SMulCommClass S R M],
  SMulCommClass S R ↥(Submodule.torsion' R M S)
-- Mathlib.NumberTheory.FermatPsp
Nat.decidablePsp : (n b : ℕ) → Decidable (n.FermatPsp b)
-- Mathlib.GroupTheory.OrderOfElement
smulCardAddSubgroup.eq_1 : ∀ {G : Type u_6} [inst : AddGroup G] [inst_1 : Fintype G] (S : Set G) (hS : S.Nonempty),
  smulCardAddSubgroup S hS = addSubgroupOfIdempotent (Fintype.card G • S) ⋯ ⋯
-- Init.Data.Int.Linear
Int.Internal.Linear.le_coeff_cert : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → ℤ → Bool
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.helper₂ : ∀ {w' : ℕ} (w : ℕ) (b : BitVec (w' + w)) {v : BitVec w'},
  BitVec.extractLsb' w w' b = v → b = v ++ BitVec.extractLsb' 0 w b
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.min!_insert_of_isEmpty : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → ∀ {k : α}, t.isEmpty = true → (t.insert k).min! = k
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.coe_zero : ∀ {M : Type u_4} [inst : AddZeroClass M] (S : AddSubmonoid M), ↑0 = 0
-- Init.Data.SInt.Basic
Int32.ofUInt32 : UInt32 → Int32
-- Mathlib.Analysis.Calculus.LogDeriv
/-- The logarithmic derivative of a finite product is the sum of the logarithmic derivatives.  -/
logDeriv_prod : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {ι : Type u_3} {s : Finset ι} {f : ι → 𝕜 → 𝕜'} {x : 𝕜},
  (∀ i ∈ s, f i x ≠ 0) →
    (∀ i ∈ s, DifferentiableAt 𝕜 (f i) x) → logDeriv (fun x => ∏ i ∈ s, f i x) x = ∑ i ∈ s, logDeriv (f i) x
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.contractibleTriangle_mor₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C] (X : C),
  (CategoryTheory.Pretriangulated.contractibleTriangle X).mor₂ = 0
-- Mathlib.RingTheory.Bialgebra.TensorProduct
/-- `lTensor A f : A ⊗ B →ₐc A ⊗ C` is the natural bialgebra morphism induced by `f : B →ₐc C`.  -/
BialgHom.lTensor : {R : Type u_1} →
  (A : Type u_2) →
    {B : Type u_3} →
      {C : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : Ring A] →
            [inst_2 : Ring B] →
              [inst_3 : Ring C] →
                [inst_4 : Bialgebra R A] →
                  [inst_5 : Bialgebra R B] →
                    [inst_6 : Bialgebra R C] → (B →ₐc[R] C) → TensorProduct R A B →ₐc[R] TensorProduct R A C
-- Mathlib.RingTheory.Extension.Presentation.Basic
/-- The index of generators to `ofFinitePresentation`.  -/
Algebra.Presentation.ofFinitePresentationVars : (R : Type u) →
  (S : Type v) →
    [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → [Algebra.FinitePresentation R S] → ℕ
-- Mathlib.GroupTheory.OrderOfElement
addOrderOf_dvd_iff_nsmul_eq_zero : ∀ {G : Type u_1} [inst : AddMonoid G] {x : G} {n : ℕ}, addOrderOf x ∣ n ↔ n • x = 0
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.unop_ι : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F.op),
  c.unop.ι = CategoryTheory.NatTrans.removeOp c.π
-- Mathlib.Order.Filter.Prod
Filter.tendsto_diag : ∀ {α : Type u_1} {f : Filter α}, Filter.Tendsto Function.diag f (f ×ˢ f)
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.forall_measure_inter_isCountablySpanning_eq_zero : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {C : Set (Set α)},
  IsCountablySpanning C → ((∀ t ∈ C, μ (s ∩ t) = 0) ↔ μ s = 0)
-- Mathlib.Algebra.Group.Irreducible.Defs
AddIrreducible.eq_zero_or_eq_zero : ∀ {M : Type u_1} [inst : AddMonoid M] {a b : M} [Subsingleton (AddUnits M)], AddIrreducible (a + b) → a = 0 ∨ b = 0