mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Sites.MorphismProperty
AlgebraicGeometry.Scheme.singleton_mem_precoverage_iff : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S),
  CategoryTheory.Presieve.singleton f ∈ (AlgebraicGeometry.Scheme.precoverage P).coverings S ↔
    Function.Surjective ⇑f ∧ P f
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.isIso_hom_iff_isIso_of_isIso : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {Y Z : T} {f : CategoryTheory.Arrow T} {g : Y ⟶ Z}
  (sq : f ⟶ CategoryTheory.Arrow.mk g) [CategoryTheory.IsIso sq], CategoryTheory.IsIso f.hom ↔ CategoryTheory.IsIso g
-- Mathlib.Order.Filter.Pointwise
Filter.instSub.eq_1 : ∀ {α : Type u_2} [inst : Sub α],
  Filter.instSub =
    {
      sub := fun f g =>
        let __src := Filter.map₂ (fun x1 x2 => x1 - x2) f g;
        { sets := {s | ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ - t₂ ⊆ s}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ } }
-- Mathlib.Algebra.Field.Rat
NNRat.num_div_den : ∀ (q : ℚ≥0), ↑q.num / ↑q.den = q
-- Mathlib.Order.SuccPred.LinearLocallyFinite
toZ.congr_simp : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : SuccOrder ι] [inst_2 : IsSuccArchimedean ι] [inst_3 : PredOrder ι]
  (i0 i0_1 : ι), i0 = i0_1 → ∀ (i i_1 : ι), i = i_1 → toZ i0 i = toZ i0_1 i_1
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.HasBiproductsOfShape.mk : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C],
  (∀ (F : J → C), CategoryTheory.Limits.HasBiproduct F) → CategoryTheory.Limits.HasBiproductsOfShape J C
-- Mathlib.Data.Finset.Max
Finset.lt_max'_of_mem_erase_max' : ∀ {α : Type u_2} [inst : LinearOrder α] (s : Finset α) (H : s.Nonempty) [inst_1 : DecidableEq α] {a : α},
  a ∈ s.erase (s.max' H) → a < s.max' H
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.mem_ofList : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [inst : Std.TransCmp cmp] [inst_1 : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List (α × β)} {k : α}, k ∈ Std.ExtDTreeMap.Const.ofList l cmp ↔ (List.map Prod.fst l).contains k = true
-- Mathlib.RepresentationTheory.Character
/-- The character of a representation is constant on conjugacy classes.  -/
Representation.char_conj : ∀ {G : Type u_1} {k : Type u_2} {V : Type u_3} [inst : Group G] [inst_1 : Field k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] (ρ : Representation k G V) (g h : G), ρ.character (h * g * h⁻¹) = ρ.character g
-- Mathlib.Logic.Encodable.Basic
_private.Mathlib.Logic.Encodable.Basic.0.Directed.sequence.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (a : α) (h_1 : Unit → motive none) (h_2 : (a : α) → motive (some a)),
  (match some a with
    | none => h_1 ()
    | some a => h_2 a) =
    h_2 a
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
/-- For any function `f : α → ℝ≥0∞`, there exists a measurable function `g ≤ f` with the same
integral.  -/
MeasureTheory.exists_measurable_le_lintegral_eq : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → ENNReal),
  ∃ g, Measurable g ∧ g ≤ f ∧ ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
_private.Mathlib.FieldTheory.IntermediateField.Adjoin.Defs.0.IntermediateField.delabAdjoinNotation.delabInsertArray : Lean.PrettyPrinter.Delaborator.DelabM (List Lean.Term)
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Over.pullbackMapHomPullback_app : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T}
  [inst_1 : Q.IsMultiplicative] [inst_2 : P.IsStableUnderComposition] {X Y Z : T} (f : X ⟶ Y) (hPf : P f) (hQf : Q f)
  (g : Y ⟶ Z) [inst_3 : P.IsStableUnderBaseChangeAlong f] [inst_4 : P.IsStableUnderBaseChangeAlong g]
  [inst_5 : Q.IsStableUnderBaseChange] [inst_6 : CategoryTheory.Limits.HasPullbacks T]
  (fg : optParam (X ⟶ Z) (CategoryTheory.CategoryStruct.comp f g))
  (hfg :
    autoParam (CategoryTheory.CategoryStruct.comp f g = fg)
      CategoryTheory.MorphismProperty.Over.pullbackMapHomPullback._auto_1)
  (A : P.Over Q Z),
  (CategoryTheory.MorphismProperty.Over.pullbackMapHomPullback f hPf hQf g fg hfg).app A =
    CategoryTheory.MorphismProperty.Over.homMk
      (CategoryTheory.Limits.pullback.map A.hom fg A.hom g (CategoryTheory.CategoryStruct.id A.left) f
        (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯)
      ⋯ ⋯
-- Mathlib.Analysis.Normed.Group.Uniform
cauchySeq_prod_of_eventually_eq : ∀ {E : Type u_2} [inst : SeminormedCommGroup E] {u v : ℕ → E} {N : ℕ},
  (∀ n ≥ N, u n = v n) →
    (CauchySeq fun n => ∏ k ∈ Finset.range (n + 1), v k) → CauchySeq fun n => ∏ k ∈ Finset.range (n + 1), u k
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryLE?_eq_getEntryGE?_reverse : ∀ {α : Type u} {β : α → Type v} [o : Ord α] [Std.TransOrd α] {t : Std.DTreeMap.Internal.Impl α β} {k : α},
  Std.DTreeMap.Internal.Impl.getEntryLE? k t = Std.DTreeMap.Internal.Impl.getEntryGE? k t.reverse
-- Batteries.Data.List.Lemmas
List.countPBefore_findIdxNth_of_lt_countP : ∀ {α : Type u_1} {n : ℕ} {p : α → Bool} {xs : List α},
  n < List.countP p xs → List.countPBefore p xs (List.findIdxNth p xs n) = n
-- Mathlib.Algebra.DirectSum.Ring
DirectSum.GNonUnitalNonAssocSemiring.toGMul : {ι : Type u_1} →
  {A : ι → Type u_2} →
    {inst : Add ι} →
      {inst_1 : (i : ι) → AddCommMonoid (A i)} → [self : DirectSum.GNonUnitalNonAssocSemiring A] → GradedMonoid.GMul A
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.forgetEval_hom_app : ∀ {ι : Type u_1} (V : Type u) [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) (i : ι) (X : HomologicalComplex V c),
  (HomologicalComplex.forgetEval V c i).hom.app X = CategoryTheory.CategoryStruct.id (X.X i)
-- Mathlib.Order.Category.Lat
Lat.Hom.ext_iff : ∀ {X Y : Lat} {x y : X.Hom Y}, x = y ↔ x.hom' = y.hom'
-- Init.Data.Option.Lemmas
Option.get_min : ∀ {α : Type u_1} [inst : Min α] {o o' : Option α} {h : (o ⊓ o').isSome = true}, (o ⊓ o').get h = o.get ⋯ ⊓ o'.get ⋯
-- Aesop.Script.StructureStatic
Aesop.Script.StaticStructureM.Context.steps : Aesop.Script.StaticStructureM.Context → Std.HashMap Lean.MVarId (ℕ × Aesop.Script.Step)
-- Init.Control.Lawful.Instances
ExceptT.run_mk : ∀ {m : Type (max u_1 u_2) → Type u_3} {ε α : Type (max u_1 u_2)} (x : m (Except ε α)), (ExceptT.mk x).run = x
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_inv_Ico : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b : α),
  Inv.inv '' Set.Ico a b = Set.Ioc b⁻¹ a⁻¹
-- Mathlib.Order.Interval.Set.Basic
Set.Icc_subset_Iic_iff : ∀ {α : Type u_1} [inst : Preorder α] {a₁ a₂ b₁ : α}, b₁ ≤ a₁ → (Set.Icc b₁ a₁ ⊆ Set.Iic a₂ ↔ a₁ ≤ a₂)
-- Mathlib.RingTheory.MvPowerSeries.Order
/-- The `n`th coefficient of a formal power series is `0` if `n` is strictly
smaller than the order of the power series.  -/
MvPowerSeries.coeff_eq_zero_of_lt_weightedOrder : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (w : σ → ℕ) {f : MvPowerSeries σ R} {d : σ →₀ ℕ},
  ↑((Finsupp.weight w) d) < MvPowerSeries.weightedOrder w f → (MvPowerSeries.coeff d) f = 0
-- Mathlib.LinearAlgebra.RootSystem.Defs
/-- Roots written as functionals on the coweight space.  -/
RootPairing.root' : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → RootPairing ι R M N → ι → Module.Dual R N
-- Init.Grind.FieldNormNum
Lean.Grind.Field.NormNum.neg_eq : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] (a : α) (v₁ v : ℚ),
  (v == -v₁) = true → a = Lean.Grind.Field.NormNum.ofRat v₁ → -a = Lean.Grind.Field.NormNum.ofRat v
-- Mathlib.Data.Multiset.MapFold
Multiset.foldr_singleton : ∀ {α : Type u_1} {β : Type v} (f : α → β → β) [inst : LeftCommutative f] (b : β) (a : α), Multiset.foldr f b {a} = f a b
-- Mathlib.Algebra.Order.Group.Unbundled.Int
Int.emod_lt_abs : ∀ (a : ℤ) {b : ℤ}, b ≠ 0 → a % b < |b|
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.adjoinRootEquivAdjoin_apply_root : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {α : E} (h : IsIntegral F α),
  (IntermediateField.adjoinRootEquivAdjoin F h) (AdjoinRoot.root (minpoly F α)) = IntermediateField.AdjoinSimple.gen F α
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
not_linearIndepOn_finset_iff : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {v : ι → M} {s : Finset ι}, ¬LinearIndepOn R v ↑s ↔ ∃ f, ∑ i ∈ s, f i • v i = 0 ∧ ∃ i ∈ s, f i ≠ 0
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
linearIndependent_iffₒₛ : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : LinearOrder R] [CanonicallyOrderedAdd R] [AddRightReflectLE R] [IsCancelAdd M],
  LinearIndependent R v ↔
    ∀ (s t : Finset ι) (f : ι → R),
      Disjoint s t → ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0
-- Lean.Meta.Sym.Simp.SimpM
/-- Configuration options for the structural simplifier.  -/
Lean.Meta.Sym.Simp.Config : Type
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearEquiv.lTensor_trans_congr : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} {S : Type u_11}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : AddCommMonoid S] [inst_6 : Module R M] [inst_7 : Module R N] [inst_8 : Module R S] [inst_9 : Module R P]
  [inst_10 : Module R Q] (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) (g' : S ≃ₗ[R] N),
  LinearEquiv.lTensor M g' ≪≫ₗ TensorProduct.congr f g = TensorProduct.congr f (g' ≪≫ₗ g)
-- Init.Data.Array.MapIdx
Array.mapFinIdx_spec : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : ℕ) → α → i < xs.size → β}
  {p : (i : ℕ) → β → i < xs.size → Prop},
  (∀ (i : ℕ) (h : i < xs.size), p i (f i xs[i] h) h) →
    ∃ (eq : (xs.mapFinIdx f).size = xs.size), ∀ (i : ℕ) (h : i < xs.size), p i (xs.mapFinIdx f)[i] h
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.ofUnique.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : Unique M] [inst_1 : Unique N] [inst_2 : Mul M] [inst_3 : Mul N]
  [inst_4 : TopologicalSpace M] [inst_5 : TopologicalSpace N],
  ContinuousMulEquiv.ofUnique = { toMulEquiv := MulEquiv.ofUnique, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Mathlib.Algebra.Colimit.Ring
Field.DirectLimit.nontrivial : ∀ {ι : Type u_1} [inst : Preorder ι] (G : ι → Type u_2) [Nonempty ι] [IsDirectedOrder ι]
  [inst_3 : (i : ι) → Field (G i)] (f' : (i j : ι) → i ≤ j → G i →+* G j)
  [DirectedSystem G fun x1 x2 x3 => ⇑(f' x1 x2 x3)], Nontrivial (Ring.DirectLimit G fun x1 x2 x3 => ⇑(f' x1 x2 x3))
-- Mathlib.RingTheory.FractionalIdeal.Inverse
FractionalIdeal.spanSingleton_mul_inv : ∀ (K : Type u_3) [inst : Field K] {R₁ : Type u_4} [inst_1 : CommRing R₁] [inst_2 : IsDomain R₁] [inst_3 : Algebra R₁ K]
  [inst_4 : IsFractionRing R₁ K] {x : K},
  x ≠ 0 →
    FractionalIdeal.spanSingleton (nonZeroDivisors R₁) x * (FractionalIdeal.spanSingleton (nonZeroDivisors R₁) x)⁻¹ = 1
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey_insertEntryIfNew : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {v : β k},
      Std.Internal.List.maxKey (Std.Internal.List.insertEntryIfNew k v l) ⋯ =
        (Std.Internal.List.maxKey? l).elim k fun k' => if compare k' k = Ordering.lt then k else k'
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ContinuousHom.mk.congr_simp : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β]
  (toOrderHom toOrderHom_1 : α →o β) (e_toOrderHom : toOrderHom = toOrderHom_1)
  (map_ωSup' :
    ∀ (c : OmegaCompletePartialOrder.Chain α),
      toOrderHom.toFun (OmegaCompletePartialOrder.ωSup c) = OmegaCompletePartialOrder.ωSup (c.map toOrderHom)),
  { toOrderHom := toOrderHom, map_ωSup' := map_ωSup' } = { toOrderHom := toOrderHom_1, map_ωSup' := ⋯ }
-- Mathlib.Algebra.Lie.Basic
/-- A Lie ring bracket satisfies a Leibniz / Jacobi identity.  -/
LieRing.leibniz_lie : ∀ {L : Type v} [self : LieRing L] (x y z : L), ⁅x, ⁅y, z⁆⁆ = ⁅⁅x, y⁆, z⁆ + ⁅y, ⁅x, z⁆⁆
-- Mathlib.Algebra.Ring.Subring.Basic
RingEquiv.restrict_apply_coe : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] {σR : Type u_1} {σS : Type u_2}
  [inst_2 : SetLike σR R] [inst_3 : SetLike σS S] [inst_4 : SubsemiringClass σR R] [inst_5 : SubsemiringClass σS S]
  (e : R ≃+* S) (s' : σR) (s : σS) (h : ∀ (x : R), x ∈ s' ↔ e x ∈ s) (a : ↥s'), ↑((e.restrict s' s h) a) = e ↑a
-- Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Asymptotics.SuperpolynomialDecay.param_pow_mul : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {k f : α → β} [inst : TopologicalSpace β] [inst_1 : CommSemiring β],
  Asymptotics.SuperpolynomialDecay l k f → ∀ (n : ℕ), Asymptotics.SuperpolynomialDecay l k (k ^ n * f)
-- Mathlib.Probability.Kernel.Disintegration.StandardBorel
ProbabilityTheory.Kernel.condKernel_def : ∀ {α : Type u_5} {β : Type u_6} {Ω : Type u_7} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] [inst_1 : Nonempty Ω]
  [h : MeasurableSpace.CountableOrCountablyGenerated α β] (κ : ProbabilityTheory.Kernel α (β × Ω))
  [inst_2 : ProbabilityTheory.IsFiniteKernel κ],
  κ.condKernel =
    if hα : Countable α then ProbabilityTheory.Kernel.condKernelCountable (fun a => (κ a).condKernel) ⋯
    else κ.condKernelBorel
-- Mathlib.InformationTheory.KullbackLeibler.KLFun
InformationTheory.not_differentiableWithinAt_klFun_Iio_zero : ¬DifferentiableWithinAt ℝ InformationTheory.klFun (Set.Iio 0) 0
-- Init.Data.Array.Basic
Array.swap.congr_simp : ∀ {α : Type u} (xs xs_1 : Array α) (e_xs : xs = xs_1) (i i_1 : ℕ) (e_i : i = i_1) (j j_1 : ℕ) (e_j : j = j_1)
  (hi : i < xs.size) (hj : j < xs.size), xs.swap i j hi hj = xs_1.swap i_1 j_1 ⋯ ⋯
-- Mathlib.GroupTheory.Perm.Cycle.Type
/-- The type of vectors with terms from `G`, length `n`, and product equal to `1:G`.  -/
Equiv.Perm.vectorsProdEqOne : (G : Type u_2) → [Group G] → (n : ℕ) → Set (List.Vector G n)
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.mem.eq_1 : ∀ {α : Type u_1} (a : FreeAddMonoid α) (m : α), a.mem m = (m ∈ FreeAddMonoid.toList a)
-- Mathlib.Data.Fintype.BigOperators
Finset.sum_fin_eq_sum_range : ∀ {β : Type u_2} [inst : AddCommMonoid β] {n : ℕ} (c : Fin n → β),
  ∑ i, c i = ∑ i ∈ Finset.range n, if h : i < n then c ⟨i, h⟩ else 0
-- Mathlib.Topology.Order.LawsonTopology
Topology.WithLawson.ofLawson_toLawson : ∀ {α : Type u_1} (a : α), Topology.WithLawson.ofLawson (Topology.WithLawson.toLawson a) = a
-- Mathlib.GroupTheory.QuotientGroup.Finite
Group.fintypeOfDomOfCoker.eq_1 : ∀ {F : Type u_1} {G : Type u_2} [inst : Group F] [inst_1 : Group G] [inst_2 : Fintype F] (f : F →* G)
  [inst_3 : f.range.Normal] [inst_4 : Fintype (G ⧸ f.range)],
  Group.fintypeOfDomOfCoker f = Group.fintypeOfKerLeRange f (QuotientGroup.mk' f.range) ⋯
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.BitVec.mul_ite_zero'' : ∀ {w : ℕ} {c : Bool} {a e : BitVec w}, (bif c then 0#w else e) * a = bif c then 0#w else e * a
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
/-- Build an isomorphism in the category `ProfiniteAddGrp` from
a `ContinuousAddEquiv` between `ProfiniteAddGrp`s.  -/
ProfiniteAddGrp.ContinuousMulEquiv.toProfiniteAddGrpIso : {X Y : ProfiniteAddGrp.{u_1}} → ↑X.toProfinite.toTop ≃ₜ+ ↑Y.toProfinite.toTop → (X ≅ Y)
-- Mathlib.CategoryTheory.Localization.Construction
CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse_obj_map : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] (W : CategoryTheory.MorphismProperty C) (D : Type uD)
  [inst_1 : CategoryTheory.Category.{uD', uD} D] (G : W.FunctorsInverting D)
  {X Y : CategoryTheory.Quotient (CategoryTheory.Localization.Construction.relations W)} (hf : X ⟶ Y),
  ((CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse W D).obj G).map hf =
    Quot.liftOn hf
      (fun f =>
        CategoryTheory.composePath
          ({ obj := fun X => G.obj.obj X.obj,
                map := fun {X Y} a =>
                  Sum.rec (fun val => G.obj.map val) (fun val => CategoryTheory.inv (G.obj.map ↑val)) a }.mapPath
            f))
      ⋯
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.exists_isConj_of_isRamified : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K] [IsGalois k K] {φ : K →+* ℂ},
  NumberField.InfinitePlace.IsRamified k (NumberField.InfinitePlace.mk φ) → ∃ σ, NumberField.ComplexEmbedding.IsConj φ σ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.of_constToArray_perm : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap.Raw α (fun x => β) cmp},
  (Std.DTreeMap.Raw.Const.toArray t₁).Perm (Std.DTreeMap.Raw.Const.toArray t₂) → t₁.Equiv t₂
-- Mathlib.NumberTheory.BernoulliPolynomials
Polynomial.bernoulli_eval_zero : ∀ (n : ℕ), Polynomial.eval 0 (Polynomial.bernoulli n) = bernoulli n
-- Mathlib.RingTheory.Ideal.GoingUp
Ideal.IsIntegral.comap_ne_bot : ∀ (R : Type u_1) [inst : CommRing R] {A : Type u_3} [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Algebra.IsIntegral R A] [IsDomain A] [Nontrivial R] {I : Ideal A}, I ≠ ⊥ → Ideal.comap (algebraMap R A) I ≠ ⊥
-- Mathlib.LinearAlgebra.Dual.Defs
Module.Dual.eval_apply : ∀ (R : Type u_1) (M : Type u_3) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (v : M)
  (a : Module.Dual R M), ((Module.Dual.eval R M) v) a = a v
-- Batteries.Lean.Except
Except.map_error : ∀ {α β : Type u_1} {ε : Type u} (f : α → β) (e : ε), f <$> Except.error e = Except.error e
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.not_infinite_real : ∀ (r : ℝ), ¬(↑r).Infinite
-- Mathlib.Data.Multiset.Bind
Multiset.add_product : ∀ {α : Type u_1} {β : Type v} (s t : Multiset α) (u : Multiset β), (s + t) ×ˢ u = s ×ˢ u + t ×ˢ u
-- Mathlib.Algebra.Category.Semigrp.Basic
AddMagmaCat.str : (self : AddMagmaCat) → Add ↑self
-- Mathlib.Algebra.Homology.HomotopyCategory.Acyclic
HomotopyCategory.mem_subcategoryAcyclic_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (X : HomotopyCategory C (ComplexShape.up ℤ)),
  HomotopyCategory.subcategoryAcyclic C X ↔
    ∀ (n : ℤ), CategoryTheory.Limits.IsZero ((HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) n).obj X)
-- Init.Data.SInt.Lemmas
ISize.two_pow_numBits_le_toInt : ∀ (x : ISize), -2 ^ (System.Platform.numBits - 1) ≤ x.toInt
-- Mathlib.Topology.Category.UniformSpace
UniformSpaceCat.Hom.mk.inj : ∀ {X : UniformSpaceCat} {Y : UniformSpaceCat} {hom' hom'_1 : { f // UniformContinuous f }},
  { hom' := hom' } = { hom' := hom'_1 } → hom' = hom'_1
-- Lean.Level
_private.Lean.Level.0.Lean.Level.updateIMax!Impl : Lean.Level → Lean.Level → Lean.Level → Lean.Level
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.inv_neg : ∀ {R : Type u} {M : Type v} [inst : DivisionRing R] [inst_1 : AddCommGroup M] [inst_2 : Module Rᵐᵒᵖ M]
  [inst_3 : Module R M] {x : TrivSqZeroExt R M}, (-x)⁻¹ = -x⁻¹
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.of_support_subset.congr_simp : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} {f f_1 : E → F} (e_f : f = f_1)
  (hf : ContDiff ℝ (↑n) f) (hsupp : Function.support f ⊆ ↑K),
  ContDiffMapSupportedIn.of_support_subset hf hsupp = ContDiffMapSupportedIn.of_support_subset ⋯ ⋯
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.mk.inj : ∀ {α : Type u_6} {β : Type u_7} {inst : Min α} {inst_1 : Min β} {inst_2 : Top α} {inst_3 : Top β}
  {toInfHom : InfHom α β} {map_top' : toInfHom.toFun ⊤ = ⊤} {toInfHom_1 : InfHom α β}
  {map_top'_1 : toInfHom_1.toFun ⊤ = ⊤},
  { toInfHom := toInfHom, map_top' := map_top' } = { toInfHom := toInfHom_1, map_top' := map_top'_1 } →
    toInfHom = toInfHom_1
-- Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
/-- **Alias** of the reverse direction of `Real.differentiableAt_negMulLog_iff`. -/
Real.differentiableAt_negMulLog : ∀ {x : ℝ}, x ≠ 0 → DifferentiableAt ℝ Real.negMulLog x
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
/-- An auxiliary definition for `descHomotopyZero`.  -/
CategoryTheory.InjectiveResolution.descHomotopyZeroZero : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {Y Z : C} →
        {I : CategoryTheory.InjectiveResolution Y} →
          {J : CategoryTheory.InjectiveResolution Z} →
            (f : I.cocomplex ⟶ J.cocomplex) →
              CategoryTheory.CategoryStruct.comp I.ι f = 0 → (I.cocomplex.X 1 ⟶ J.cocomplex.X 0)
-- Mathlib.Order.Filter.Basic
Filter.principal_mono : ∀ {α : Type u} {s t : Set α}, Filter.principal s ≤ Filter.principal t ↔ s ⊆ t
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.right_le_veblen : ∀ (o a : Ordinal.{u_1}), a ≤ Ordinal.veblen o a
-- Mathlib.CategoryTheory.Comma.Over.Pullback
CategoryTheory.Over.mapPullbackAdj_unit_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPullbacksAlong f] (X_1 : CategoryTheory.Over X),
  (CategoryTheory.Over.mapPullbackAdj f).unit.app X_1 =
    CategoryTheory.Over.homMk
      (CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.id X_1.left) X_1.hom ⋯) ⋯
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.ae_eq_restrict_biUnion_iff : ∀ {α : Type u_2} {δ : Type u_4} {ι : Type u_6} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : ι → Set α)
  {t : Set ι}, t.Countable → ∀ (f g : α → δ), f =ᵐ[μ.restrict (⋃ i ∈ t, s i)] g ↔ ∀ i ∈ t, f =ᵐ[μ.restrict (s i)] g
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
/-- `C₀(α, β)` is the type of continuous functions `α → β` which vanish at infinity from a
topological space to a metric space with a zero element.

When possible, instead of parametrizing results over `(f : C₀(α, β))`,
you should parametrize over `(F : Type*) [ZeroAtInftyContinuousMapClass F α β] (f : F)`.

When you extend this structure, make sure to extend `ZeroAtInftyContinuousMapClass`.  -/
ZeroAtInfty.«term_→C₀_» : Lean.TrailingParserDescr
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
/-- The symmetric product of vectors is a scalar  -/
CliffordAlgebra.ι_mul_ι_add_swap : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (a b : M),
  (CliffordAlgebra.ι Q) a * (CliffordAlgebra.ι Q) b + (CliffordAlgebra.ι Q) b * (CliffordAlgebra.ι Q) a =
    (algebraMap R (CliffordAlgebra Q)) (QuadraticMap.polar (⇑Q) a b)
-- Init.SimpLemmas
iff_true : ∀ (p : Prop), (p ↔ True) = p
-- Mathlib.NumberTheory.Modular
ModularGroup.lcRow0Extend_symm_apply : ∀ {cd : Fin 2 → ℤ} (hcd : IsCoprime (cd 0) (cd 1)) (f : (i : Fin 2) → (fun a => Fin 2 → ℝ) i) (i a : Fin 2),
  (ModularGroup.lcRow0Extend hcd).symm f i a =
    (![(LinearMap.GeneralLinearGroup.generalLinearEquiv ℝ (Fin 2 → ℝ))
              (Matrix.GeneralLinearGroup.toLin (Matrix.planeConformalMatrix (↑(cd 0)) (-↑(cd 1)) ⋯)),
            LinearEquiv.refl ℝ (Fin 2 → ℝ)]
          i).symm
      (f i) a
-- Mathlib.Topology.Order
instDiscreteTopologyBool : DiscreteTopology Bool
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
/-- As `x → 0`, we have `f x = x ^ (-P.k) • constant` up to a rapidly decaying error.  -/
WeakFEPair.hf_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (P : WeakFEPair E) (r : ℝ),
  (fun x => P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) =O[nhdsWithin 0 (Set.Ioi 0)] fun x => x ^ r
-- Mathlib.Condensed.Light.Instances
LightProfinite.hasSheafify_type : CategoryTheory.HasSheafify (CategoryTheory.coherentTopology LightProfinite) (Type u)