mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Free
FreeAddMagma.toFreeAddSemigroup_comp_map : ∀ {α : Type u} {β : Type v} (f : α → β),
  FreeAddMagma.toFreeAddSemigroup.comp (FreeAddMagma.map f) =
    (FreeAddSemigroup.map f).comp FreeAddMagma.toFreeAddSemigroup
-- Mathlib.Combinatorics.Quiver.Prefunctor
Prefunctor.comp_map : ∀ {U : Type u_1} [inst : Quiver U] {V : Type u_2} [inst_1 : Quiver V] {W : Type u_3} [inst_2 : Quiver W] (F : U ⥤q V)
  (G : V ⥤q W) {X Y : U} (f : X ⟶ Y), (F ⋙q G).map f = G.map (F.map f)
-- Mathlib.GroupTheory.Goursat
/-- For `I` a subgroup of `G × H`, `I.goursatSnd` is the kernel of the projection map `I → G`,
considered as a subgroup of `H`.

This is the second subgroup appearing in Goursat's lemma. See `Subgroup.goursat`.  -/
Subgroup.goursatSnd : {G : Type u_1} → {H : Type u_2} → [inst : Group G] → [inst_1 : Group H] → Subgroup (G × H) → Subgroup H
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.instBEqExtraTheorem : BEq Lean.Elab.Tactic.Grind.ExtraTheorem
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.shortComplexFunctor'_obj_f : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} (c : ComplexShape ι) (i j k : ι) (K : HomologicalComplex C c),
  ((HomologicalComplex.shortComplexFunctor' C c i j k).obj K).f = K.d i j
-- Mathlib.CategoryTheory.Sites.PreservesSheafification
CategoryTheory.sheafComposeIso_inv_fac : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1}
  {B : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_1} A] [inst_2 : CategoryTheory.Category.{v_2, u_2} B]
  (F : CategoryTheory.Functor A B) [inst_3 : CategoryTheory.HasWeakSheafify J A]
  [inst_4 : CategoryTheory.HasWeakSheafify J B] [inst_5 : J.HasSheafCompose F] [inst_6 : J.PreservesSheafification F]
  (P : CategoryTheory.Functor Cᵒᵖ A),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.toSheafify J P) F)
      (CategoryTheory.sheafifyComposeIso J F P).inv =
    CategoryTheory.toSheafify J (P.comp F)
-- Init.Data.Int.Basic
instCoeTailIntOfIntCast : {R : Type u_1} → [IntCast R] → CoeTail ℤ R
-- Init.Data.Array.Lemmas
Array.append_eq_singleton_iff : ∀ {α : Type u_1} {xs ys : Array α} {x : α}, xs ++ ys = #[x] ↔ xs = #[] ∧ ys = #[x] ∨ xs = #[x] ∧ ys = #[]
-- Batteries.Data.Random.MersenneTwister
_private.Batteries.Data.Random.MersenneTwister.0.Batteries.Random.MersenneTwister.Config.uMask : (cfg : Batteries.Random.MersenneTwister.Config) → BitVec cfg.wordSize
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.omega0_lt_gamma : ∀ (o : Ordinal.{u_1}), Ordinal.omega0 < o.gamma
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.Weight.hasEigenvalueAt : ∀ {R : Type u_2} {L : Type u_3} {M : Type u_4} [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]
  [inst_7 : LieRing.IsNilpotent L] (χ : LieModule.Weight R L M) (x : L), ((LieModule.toEnd R L M) x).HasEigenvalue (χ x)
-- Mathlib.Order.Category.BddDistLat
BddDistLat.ofHom_comp : ∀ {X Y Z : Type u} [inst : DistribLattice X] [inst_1 : BoundedOrder X] [inst_2 : DistribLattice Y]
  [inst_3 : BoundedOrder Y] [inst_4 : DistribLattice Z] [inst_5 : BoundedOrder Z] (f : BoundedLatticeHom X Y)
  (g : BoundedLatticeHom Y Z),
  BddDistLat.ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (BddDistLat.ofHom f) (BddDistLat.ofHom g)
-- Mathlib.FieldTheory.SeparableClosure
/-- The normal closure in `E/F` of the separable closure of `F` in `E` is equal to itself.  -/
separableClosure.normalClosure_eq_self : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
  IntermediateField.normalClosure F (↥(separableClosure F E)) E = separableClosure F E
-- Init.Data.Slice.Array.Lemmas
Subarray.toArray_toList : ∀ {α : Type u_1} {xs : Subarray α}, (Std.Slice.toList xs).toArray = Std.Slice.toArray xs
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_assoc : ∀ {B : Type u₁} {C : Type u₂} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  [inst_2 : CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁)
  (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃)
  (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
  (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f) {Z : F.obj b₀ ⟶ F.obj b₃} (h : F.map f ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯).inv h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom (F.map f₂₃))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv)
          (CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯).inv h)))
-- LeanSearchClient.Syntax
LeanSearchClient.useragent : Lean.CoreM String
-- Mathlib.Data.Fintype.Sets
/-- **Alias** of `Set.toFinset_sdiff`. -/
Set.toFinset_diff : ∀ {α : Type u_1} (s t : Set α) [inst : DecidableEq α] [inst_1 : Fintype ↑s] [inst_2 : Fintype ↑t]
  [inst_3 : Fintype ↑(s \ t)], (s \ t).toFinset = s.toFinset \ t.toFinset
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.surjective_unitGroupToResidueFieldUnits : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K), Function.Surjective ⇑A.unitGroupToResidueFieldUnits
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.measure_symmDiff_ne_top : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s t : Set α},
  μ s ≠ ⊤ → μ t ≠ ⊤ → μ (symmDiff s t) ≠ ⊤
-- Mathlib.Order.Filter.Lift
Filter.lift_principal : ∀ {α : Type u_1} {β : Type u_2} {g : Set α → Filter β} {s : Set α}, Monotone g → (Filter.principal s).lift g = g s
-- Mathlib.Algebra.Polynomial.Div
Polynomial.associated_of_dvd_of_natDegree_le : ∀ {K : Type u_1} [inst : Field K] {p q : Polynomial K}, p ∣ q → q ≠ 0 → q.natDegree ≤ p.natDegree → Associated p q
-- Mathlib.Topology.Separation.Basic
ULift.instT0Space : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T0Space X], T0Space (ULift.{u_3, u_1} X)
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.spanning_iff_closure_eq : ∀ {α : Type u_2} {M : Matroid α} {S : Set α},
  autoParam (S ⊆ M.E) Matroid.spanning_iff_closure_eq._auto_1 → (M.Spanning S ↔ M.closure S = M.E)
-- Mathlib.Analysis.Normed.Group.Constructions
Multiplicative.seminormedAddCommGroup : {E : Type u_2} → [SeminormedAddCommGroup E] → SeminormedCommGroup (Multiplicative E)
-- Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Homotopy.extend.hom_eq_zero₂ : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Preadditive C] {K L : HomologicalComplex C c} (e : c.Embedding c')
  (φ : (i j : ι) → K.X i ⟶ L.X j) (i' j' : ι'), (∀ (j : ι), e.f j ≠ j') → Homotopy.extend.hom e φ i' j' = 0
-- Lean.Parser.Term
Lean.Parser.Term.completion.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Meta.Defs
Lean.Meta.Omega.OmegaConfig.mk.injEq : ∀
  (splitDisjunctions splitNatSub splitNatAbs splitMinMax splitDisjunctions_1 splitNatSub_1 splitNatAbs_1 splitMinMax_1 :
    Bool),
  ({ splitDisjunctions := splitDisjunctions, splitNatSub := splitNatSub, splitNatAbs := splitNatAbs,
        splitMinMax := splitMinMax } =
      { splitDisjunctions := splitDisjunctions_1, splitNatSub := splitNatSub_1, splitNatAbs := splitNatAbs_1,
        splitMinMax := splitMinMax_1 }) =
    (splitDisjunctions = splitDisjunctions_1 ∧
      splitNatSub = splitNatSub_1 ∧ splitNatAbs = splitNatAbs_1 ∧ splitMinMax = splitMinMax_1)
-- Mathlib.Topology.CompactOpen
/-- If `g : C(Y, Z)` is a topological embedding,
then the composition `ContinuousMap.comp g : C(X, Y) → C(X, Z)` is an embedding too.  -/
ContinuousMap.isEmbedding_postcomp : ∀ {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (g : C(Y, Z)), Topology.IsEmbedding ⇑g → Topology.IsEmbedding g.comp
-- Mathlib.Analysis.Analytic.Inverse
FormalMultilinearSeries.rightInv_coeff_one : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E),
  p.rightInv i x 1 = (continuousMultilinearCurryFin1 𝕜 F E).symm ↑i.symm
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- Given a finite family of pairwise disjoint finsets, the product over their union is the product
of the products over the sets.
See also `prod_biUnion_of_pairwise_eq_one` for a version with weaker assumptions.  -/
Finset.prod_biUnion : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : CommMonoid M] {f : ι → M} [inst_1 : DecidableEq ι] {s : Finset κ}
  {t : κ → Finset ι}, (↑s).PairwiseDisjoint t → ∏ x ∈ s.biUnion t, f x = ∏ x ∈ s, ∏ i ∈ t x, f i
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Mon.instZeroHom.eq_1 : ∀ {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} D] [inst_1 : CategoryTheory.SemiCartesianMonoidalCategory D]
  (M N : CategoryTheory.Mon D),
  M.instZeroHom N =
    {
      zero :=
        {
          hom :=
            CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit M.X)
              CategoryTheory.MonObj.one,
          isMonHom_hom := ⋯ } }
-- Init.Data.Int.DivMod.Lemmas
Int.bmod_add_bdiv : ∀ (x : ℤ) (m : ℕ), x.bmod m + ↑m * x.bdiv m = x
-- Mathlib.Topology.Connected.PathConnected
JoinedIn.target_mem : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} {F : Set X}, JoinedIn F x y → y ∈ F
-- Init.Data.UInt.Lemmas
instLawfulIdentityUSizeHAddOfNat : Std.LawfulIdentity (fun x1 x2 => x1 + x2) 0
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- `I ^ n ⧸ I ^ (n + 1)` can be viewed as a quotient module and as ideal of `R ⧸ I ^ (n + 1)`.
This definition gives the equivalence between the two, instead of the `R`-linear equivalence,
to bypass typeclass synthesis issues on complex `Module` goals.  -/
Ideal.powQuotPowSuccEquivMapMkPowSuccPow : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) → (n : ℕ) → ↥(I ^ n) ⧸ I • ⊤ ≃ ↥(Ideal.map (Ideal.Quotient.mk (I ^ (n + 1))) (I ^ n))
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyMapData.leftHomologyMap_comm : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData}
  (γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂) [inst_2 : S₁.HasLeftHomology]
  [inst_3 : S₂.HasLeftHomology],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap φ) h₂.leftHomologyIso.hom =
    CategoryTheory.CategoryStruct.comp h₁.leftHomologyIso.hom γ.φH
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.prod_update_of_mem : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] [inst_1 : DecidableEq ι] {s : Finset ι} {i : ι},
  i ∈ s → ∀ (f : ι → M) (b : M), ∏ x ∈ s, Function.update f i b x = b * ∏ x ∈ s \ {i}, f x
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.sup_inf_distrib_right : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] (a b c : CauSeq α abs),
  a ⊓ b ⊔ c = (a ⊔ c) ⊓ (b ⊔ c)
-- Mathlib.Algebra.Category.HopfAlgCat.Basic
_private.Mathlib.Algebra.Category.HopfAlgCat.Basic.0.HopfAlgCat.mk.inj : ∀ {R : Type u} {inst : CommRing R} {carrier : Type v} {instRing : Ring carrier}
  {instHopfAlgebra : HopfAlgebra R carrier} {carrier_1 : Type v} {instRing_1 : Ring carrier_1}
  {instHopfAlgebra_1 : HopfAlgebra R carrier_1},
  { carrier := carrier, instRing := instRing, instHopfAlgebra := instHopfAlgebra } =
      { carrier := carrier_1, instRing := instRing_1, instHopfAlgebra := instHopfAlgebra_1 } →
    carrier = carrier_1 ∧ instRing ≍ instRing_1 ∧ instHopfAlgebra ≍ instHopfAlgebra_1
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- The forgetful functor mapping an arrow to its domain.  -/
CategoryTheory.Under.forget : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] → (X : T) → CategoryTheory.Functor (CategoryTheory.Under X) T
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
CategoryTheory.Limits.PreservesLimitPair.iso_inv_snd : ∀ {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) [inst_2 : CategoryTheory.Limits.HasBinaryProduct X Y]
  [inst_3 : CategoryTheory.Limits.HasBinaryProduct (G.obj X) (G.obj Y)]
  [inst_4 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair X Y) G],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesLimitPair.iso G X Y).inv
      (G.map CategoryTheory.Limits.prod.snd) =
    CategoryTheory.Limits.prod.snd
-- Mathlib.Order.Interval.Set.WithBotTop
WithBot.image_coe_Ici : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, WithBot.some '' Set.Ici a = Set.Ici ↑a
-- Mathlib.Algebra.BigOperators.Finprod
finprod_cond_eq_prod_of_cond_iff : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] (f : α → M) {p : α → Prop} {t : Finset α},
  (∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)) → ∏ᶠ (i : α) (_ : p i), f i = ∏ i ∈ t, f i
-- Mathlib.Algebra.Category.Ring.FilteredColimits
/-- The cocone over the proposed colimit commutative semiring.  -/
CommSemiRingCat.FilteredColimits.colimitCocone : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [CategoryTheory.IsFiltered J] → (F : CategoryTheory.Functor J CommSemiRingCat) → CategoryTheory.Limits.Cocone F
-- Mathlib.LinearAlgebra.UnitaryGroup
Matrix.UnitaryGroup.transpose_coe : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {α : Type v} [inst_2 : CommRing α] [inst_3 : StarRing α]
  (U : ↥(Matrix.unitaryGroup n α)), ↑(Matrix.UnitaryGroup.transpose U) = (↑U).transpose
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey?_eq_some_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp], t.WF → ∀ {k : α}, t.contains k = true → t.getKey? k = some k
-- Mathlib.Topology.Algebra.Group.Basic
/-- **Alias** of the forward direction of `tendsto_sub_nhds_zero_iff_eq`. -/
eq_of_tendsto_sub_nhds_zero : ∀ {G : Type w} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] {α : Type u_1} {l : Filter α}
  [l.NeBot] [T2Space G] {f g : α → G} {a b : G},
  Filter.Tendsto f l (nhds a) → Filter.Tendsto g l (nhds b) → Filter.Tendsto (fun x => f x - g x) l (nhds 0) → a = b
-- Mathlib.AlgebraicGeometry.Geometrically.Irreducible
AlgebraicGeometry.Scheme.Hom.irreducibleComponentsEquiv_apply_coe : ∀ {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) [inst : AlgebraicGeometry.GeometricallyIrreducible f] (hf : IsOpenMap ⇑f)
  (a : ↑(irreducibleComponents ↥X)), ↑((AlgebraicGeometry.Scheme.Hom.irreducibleComponentsEquiv f hf) a) = ⇑f '' ↑a
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.map_of_injective : ∀ {M : Type u_1} {N : Type u_2} {F : Type u_6} [inst : CommMonoid M] [inst_1 : CommMonoid N] {k : ℕ} {ζ : M} {f : F}
  [inst_2 : FunLike F M N] [MonoidHomClass F M N], IsPrimitiveRoot ζ k → Function.Injective ⇑f → IsPrimitiveRoot (f ζ) k
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
/-- Constructor for localizer morphisms given by a functor `F : C₁ ⥤ C₂`
under the stronger assumption that the classes of morphisms `W₁` and `W₂`
satisfy `W₁ = W₂.inverseImage F`.  -/
CategoryTheory.LocalizerMorphism.ofEq : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
        {W₁ : CategoryTheory.MorphismProperty C₁} →
          {W₂ : CategoryTheory.MorphismProperty C₂} →
            {F : CategoryTheory.Functor C₁ C₂} → W₁ = W₂.inverseImage F → CategoryTheory.LocalizerMorphism W₁ W₂
-- Mathlib.RingTheory.Valuation.Integers
Valuation.Integers.eq_algebraMap_or_inv_eq_algebraMap : ∀ {F : Type u} {Γ₀ : Type v} [inst : Field F] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {v : Valuation F Γ₀}
  {O : Type w} [inst_2 : CommRing O] [inst_3 : Algebra O F],
  v.Integers O → ∀ (x : F), ∃ a, x = (algebraMap O F) a ∨ x⁻¹ = (algebraMap O F) a
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.mem_of_mem_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k a : α} {v : β},
  a ∈ t.insertIfNew k v → cmp k a ≠ Ordering.eq → a ∈ t
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.isEmpty_eq_match_step : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [inst_1 : Std.IteratorLoop α Id Id] [Std.Iterators.Productive α Id]
  [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β},
  it.isEmpty =
    match ↑it.step with
    | Std.IterStep.yield it out => false
    | Std.IterStep.skip it' => it'.isEmpty
    | Std.IterStep.done => true
-- Mathlib.Analysis.Normed.Order.Hom.Basic
GroupNormClass.toNormedGroup.eq_1 : ∀ {F : Type u_1} {α : Type u_2} [inst : FunLike F α ℝ] [inst_1 : Group α] [inst_2 : GroupNormClass F α ℝ] (f : F),
  GroupNormClass.toNormedGroup f =
    { toNorm := (GroupSeminormClass.toSeminormedGroup f).toNorm,
      toGroup := (GroupSeminormClass.toSeminormedGroup f).toGroup,
      toPseudoMetricSpace := (GroupSeminormClass.toSeminormedGroup f).toPseudoMetricSpace, eq_of_dist_eq_zero := ⋯,
      dist_eq := ⋯ }
-- Init.Data.Range.Polymorphic.PRange
/-- This type class ensures that the intersection according to `Roi.HasRcoIntersection`
of two ranges contains exactly those elements that are contained in both ranges.
 -/
Std.Roi.LawfulRcoIntersection : (α : Type w) → [LT α] → [LE α] → [Std.Roi.HasRcoIntersection α] → Prop
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.CountableOrCountablyGenerated.mk : ∀ {α : Type u_5} {β : Type u_6} [inst : MeasurableSpace β],
  Countable α ∨ MeasurableSpace.CountablyGenerated β → MeasurableSpace.CountableOrCountablyGenerated α β
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.mul_def : ∀ {M : Type u_4} [inst : MulOneClass M] (S : Submonoid M) (x y : ↥S), x * y = ⟨↑x * ↑y, ⋯⟩
-- Mathlib.Topology.Algebra.Monoid
/-- Eta-expanded form of `ContinuousAt.pow` -/
ContinuousAt.fun_pow : ∀ {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M] [inst_2 : Monoid M]
  [ContinuousMul M] {f : X → M} {x : X}, ContinuousAt f x → ∀ (n : ℕ), ContinuousAt (fun i => f i ^ n) x
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.map_id_comp : ∀ {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {D : Type uD} {F : Type uF} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : Algebra R S] [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A]
  [inst_6 : IsScalarTower R S A] [inst_7 : Semiring B] [inst_8 : Algebra R B] [inst_9 : Semiring D]
  [inst_10 : Algebra R D] [inst_11 : Semiring F] [inst_12 : Algebra R F] (g₂ : D →ₐ[R] F) (g₁ : B →ₐ[R] D),
  Algebra.TensorProduct.map (AlgHom.id S A) (g₂.comp g₁) =
    (Algebra.TensorProduct.map (AlgHom.id S A) g₂).comp (Algebra.TensorProduct.map (AlgHom.id S A) g₁)
-- Init.Core
/-- Fully universe-polymorphic dependent pairs, in which the second element's type depends on the value
of the first element and both types are allowed to be propositions. The type `PSigma β` is typically
written `Σ' a : α, β a` or `(a : α) ×' β a`.

In practice, this generality leads to universe level constraints that are difficult to solve, so
`PSigma` is rarely used in manually-written code. It is usually only used in automation that
constructs pairs of arbitrary types.

To pair a value with a proof that a predicate holds for it, use `Subtype`. To demonstrate that a
value exists that satisfies a predicate, use `Exists`. A dependent pair with a proposition as its
first component is not typically useful due to proof irrelevance: there's no point in depending on a
specific proof because all proofs are equal anyway.
 -/
PSigma : {α : Sort u} → (α → Sort v) → Sort (max (max 1 u) v)
-- Mathlib.RingTheory.DedekindDomain.Basic
/-- A ring `R` has Krull dimension at most one if all nonzero prime ideals are maximal.  -/
Ring.DimensionLEOne : (R : Type u_1) → [CommRing R] → Prop
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
nnnorm_cfc_nnreal_lt : ∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : NormedAlgebra ℝ A] [inst_3 : PartialOrder A]
  [inst_4 : StarOrderedRing A] [inst_5 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_6 : NonnegSpectrumClass ℝ A] {f : NNReal → NNReal} {a : A} {c : NNReal},
  0 < c → (∀ x ∈ spectrum NNReal a, f x < c) → ‖cfc f a‖₊ < c
-- Mathlib.Algebra.Group.Basic
mul_div_right_comm : ∀ {α : Type u_1} [inst : DivisionCommMonoid α] (a b c : α), a * b / c = a / c * b
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
/-- the first projection `Y j ⟶ X i₁`  -/
CategoryTheory.Functor.PreOneHypercoverDenseData.p₁ : {C₀ : Type u₀} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v₀, u₀} C₀] →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor C₀ C} →
          {S : C} →
            (self : F.PreOneHypercoverDenseData S) → ⦃i₁ i₂ : self.I₀⦄ → (j : self.I₁ i₁ i₂) → self.Y j ⟶ self.X i₁
-- Mathlib.Order.SymmDiff
bihimp_bihimp_sup : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] (a b : α), bihimp (bihimp a b) (a ⊔ b) = a ⊓ b
-- Init.Data.Array.Bootstrap
Array.foldlM.loop.eq_def : ∀ {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (f : β → α → m β) (as : Array α) (stop : ℕ)
  (h : stop ≤ as.size) (i j : ℕ) (b : β),
  Array.foldlM.loop f as stop h i j b =
    if hlt : j < stop then
      match i with
      | 0 => pure b
      | i'.succ =>
        have this := ⋯;
        do
        let __do_lift ← f b as[j]
        Array.foldlM.loop f as stop h i' (j + 1) __do_lift
    else pure b
-- Mathlib.RingTheory.IsAdjoinRoot
/-- `IsAdjoinRootMonic.coeff h x i` is the `i`th coefficient of the representative of `x : S`.
 -/
IsAdjoinRootMonic.coeff : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : Ring S] → {f : Polynomial R} → [inst_2 : Algebra R S] → IsAdjoinRootMonic S f → S →ₗ[R] ℕ → R
-- Mathlib.LinearAlgebra.BilinearForm.DualLattice
LinearMap.BilinForm.mem_dualSubmodule : ∀ {R : Type u_1} {S : Type u_3} {M : Type u_2} [inst : CommRing R] [inst_1 : Field S] [inst_2 : AddCommGroup M]
  [inst_3 : Algebra R S] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M]
  (B : LinearMap.BilinForm S M) {N : Submodule R M} {x : M}, x ∈ B.dualSubmodule N ↔ ∀ y ∈ N, (B x) y ∈ 1
-- Mathlib.Algebra.Module.Congruence.Defs
/-- The quotient by a congruence relation preserving additive action.  -/
VAddCon.Quotient : {S : Type u_2} → (M : Type u_3) → [inst : VAdd S M] → VAddCon S M → Type u_3
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.instNSMulQuotientNat.eq_1 : ∀ {M : Type u_4} [inst : AddMonoid M] (c : AddCon M),
  c.instNSMulQuotientNat = { smul := fun n x => Quotient.map' (fun x => n • x) ⋯ x }
-- Mathlib.CategoryTheory.Subfunctor.Equalizer
CategoryTheory.Subfunctor.equalizer.lift_ι'_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F₁ F₂ : CategoryTheory.Functor C (Type w)}
  {A : CategoryTheory.Subfunctor F₁} (f g : A.toFunctor ⟶ F₂) {G : CategoryTheory.Functor C (Type w)}
  (φ : G ⟶ A.toFunctor) (w : CategoryTheory.CategoryStruct.comp φ f = CategoryTheory.CategoryStruct.comp φ g)
  {Z : CategoryTheory.Functor C (Type w)} (h : F₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Subfunctor.equalizer.lift f g φ w)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Subfunctor.equalizer f g).ι h) =
    CategoryTheory.CategoryStruct.comp φ (CategoryTheory.CategoryStruct.comp A.ι h)