mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.Walk.length.eq_1 : ∀ {V : Type u} {G : SimpleGraph V} {u : V}, SimpleGraph.Walk.nil.length = 0
-- Mathlib.Algebra.Module.LinearMap.End
Module.End.isUnit_apply_inv_apply_of_isUnit : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {f : Module.End R M} (h : IsUnit f) (x : M), f (h.unit.inv x) = x
-- Mathlib.Topology.MetricSpace.Contracting
ContractingWith.tendsto_iterate_efixedPoint : ∀ {α : Type u_1} [inst : EMetricSpace α] {K : NNReal} {f : α → α} [inst_1 : CompleteSpace α] (hf : ContractingWith K f)
  {x : α} (hx : edist x (f x) ≠ ⊤),
  Filter.Tendsto (fun n => f^[n] x) Filter.atTop (nhds (ContractingWith.efixedPoint f hf x hx))
-- Mathlib.Order.WellFoundedSet
Set.WellFoundedOn.sigma_lex_of_wellFoundedOn_fiber : ∀ {ι : Type u_1} {γ : Type u_4} {π : ι → Type u_5} {rι : ι → ι → Prop} {rπ : (i : ι) → π i → π i → Prop} {f : γ → ι}
  {g : (i : ι) → γ → π i} {s : Set γ},
  s.WellFoundedOn (Function.onFun rι f) →
    (∀ (i : ι), (s ∩ f ⁻¹' {i}).WellFoundedOn (Function.onFun (rπ i) (g i))) →
      s.WellFoundedOn (Function.onFun (Sigma.Lex rι rπ) fun c => ⟨f c, g (f c) c⟩)
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Parser.phaseUnsafe : Lean.ParserDescr
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.le_sub_of_add_le : ∀ {a b c : Ordinal.{u_4}}, b + c ≤ a → c ≤ a - b
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.map_equiv_eq_comap_symm : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G ≃* N) (K : Subgroup G),
  Subgroup.map (↑f) K = Subgroup.comap (↑f.symm) K
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.map_id : ∀ {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  (v : MeasureTheory.VectorMeasure α M), v.map id = v
-- Mathlib.RingTheory.RingHom.Flat
RingHom.Flat.isStableUnderBaseChange : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => RingHom.Flat
-- Mathlib.Algebra.Polynomial.Derivation
Polynomial.mkDerivation_one_eq_derivative : ∀ (R : Type u_1) [inst : CommSemiring R] (f : Polynomial R), ((Polynomial.mkDerivation R) 1) f = Polynomial.derivative f
-- Mathlib.Algebra.Group.Irreducible.Lemmas
addIrreducible_add_isAddUnit : ∀ {M : Type u_2} [inst : AddMonoid M] {x y : M}, IsAddUnit x → (AddIrreducible (y + x) ↔ AddIrreducible y)
-- Mathlib.Topology.Order.SuccPred
PredOrder.isOpen_iff : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α] [PredOrder α] [NoMinOrder α]
  {s : Set α}, IsOpen s ↔ ∀ o ∈ s, Order.IsPredLimit o → ∃ a, o < a ∧ Set.Ioo o a ⊆ s
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.X.instMonoid : {q : ℕ} → Monoid (LucasLehmer.X q)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get!_eq_get!_get? : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β],
  m.WF → ∀ {a : α}, Std.DHashMap.Raw.Const.get! m a = (Std.DHashMap.Raw.Const.get? m a).get!
-- Mathlib.Analysis.CStarAlgebra.Matrix
Matrix.coe_toEuclideanCLM_eq_toEuclideanLin : ∀ {𝕜 : Type u_1} {n : Type u_3} [inst : RCLike 𝕜] [inst_1 : Fintype n] [inst_2 : DecidableEq n] (A : Matrix n n 𝕜),
  ↑(Matrix.toEuclideanCLM A) = Matrix.toEuclideanLin A
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.adj_injective : ∀ {V : Type u}, Function.Injective SimpleGraph.Adj
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.mem_union_iff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₁ ∪ m₂ ↔ k ∈ m₁ ∨ k ∈ m₂
-- Mathlib.RepresentationTheory.Invariants
Representation.mem_invariants : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommRing k] [inst_1 : Group G] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] (ρ : Representation k G V) (v : V), v ∈ ρ.invariants ↔ ∀ (g : G), (ρ g) v = v
-- Mathlib.RingTheory.Spectrum.Prime.Topology
MaximalSpectrum.toPiLocalizationEquiv_apply : ∀ (R : Type u) [inst : CommSemiring R] [inst_1 : DiscreteTopology (PrimeSpectrum R)] (x : R),
  (MaximalSpectrum.toPiLocalizationEquiv R) x = (algebraMap R (MaximalSpectrum.PiLocalization R)) x
-- Mathlib.RingTheory.DividedPowers.Padic
DividedPowers.ofInjective.eq_1 : ∀ {A : Type u_1} {B : Type u_2} [inst : CommSemiring A] [inst_1 : CommSemiring B] (I : Ideal A) (J : Ideal B)
  (f : A →+* B) (hf : Function.Injective ⇑f) (hJ : DividedPowers J) (hIJ : Ideal.map f I = J)
  (hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ y, ∃ (_ : n ≠ 0 → y ∈ I), f y = hJ.dpow n (f x)),
  DividedPowers.ofInjective I J f hf hJ hIJ hmem =
    { dpow := fun n x => if hx : x ∈ I then ⋯.choose else 0, dpow_null := ⋯, dpow_zero := ⋯, dpow_one := ⋯,
      dpow_mem := ⋯, dpow_add := ⋯, dpow_mul := ⋯, mul_dpow := ⋯, dpow_comp := ⋯ }
-- Init.Data.Array.Lemmas
Array.prod_eq_foldl : ∀ {α : Type u_1} [inst : One α] [inst_1 : Mul α] [Std.Associative fun x1 x2 => x1 * x2]
  [Std.LawfulIdentity (fun x1 x2 => x1 * x2) 1] {xs : Array α}, xs.prod = Array.foldl (fun x1 x2 => x1 * x2) 1 xs
-- Mathlib.Algebra.Order.CompleteField
/-- The isomorphism of ordered rings between two conditionally complete linearly ordered fields.  -/
ConditionallyCompleteLinearOrderedField.inducedOrderRingIso : (β : Type u_3) →
  (γ : Type u_4) →
    [inst : Field β] →
      [inst_1 : ConditionallyCompleteLinearOrder β] →
        [IsStrictOrderedRing β] →
          [inst_3 : Field γ] → [inst_4 : ConditionallyCompleteLinearOrder γ] → [IsStrictOrderedRing γ] → β ≃+*o γ
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Iso.symm_toHom_comp_toHom : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G'),
  f.symm.toHom.comp f.toHom = SimpleGraph.Hom.id
-- Mathlib.RingTheory.HahnSeries.Lex
FiniteArchimedeanClass.liftOrderHom.congr_simp : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {α : Type u_2}
  [inst_3 : PartialOrder α] (f f_1 : { a // a ≠ 0 } → α) (e_f : f = f_1)
  (h : ∀ (a b : { a // a ≠ 0 }), FiniteArchimedeanClass.mk ↑a ⋯ ≤ FiniteArchimedeanClass.mk ↑b ⋯ → f a ≤ f b),
  FiniteArchimedeanClass.liftOrderHom f h = FiniteArchimedeanClass.liftOrderHom f_1 ⋯
-- Aesop.Tree.ExtractProof
_private.Aesop.Tree.ExtractProof.0.Aesop.SafePrefixState.mk.inj : ∀ {goals goals_1 : Array Lean.MVarId}, { goals := goals } = { goals := goals_1 } → goals = goals_1
-- Init.Data.SInt.Lemmas
instAssociativeInt32HAdd : Std.Associative fun x1 x2 => x1 + x2
-- Mathlib.Analysis.SpecialFunctions.Log.Deriv
Real.log_div_le_sum_range_add : ∀ {x : ℝ},
  0 ≤ x →
    x < 1 →
      ∀ (n : ℕ),
        1 / 2 * Real.log ((1 + x) / (1 - x)) ≤
          ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (2 * ↑i + 1) + x ^ (2 * n + 1) / (1 - x ^ 2)
-- Mathlib.CategoryTheory.Limits.Shapes.KernelPair
CategoryTheory.IsKernelPair.mono_of_isIso_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {R X Y : C} {f : X ⟶ Y} {a b : R ⟶ X},
  CategoryTheory.IsKernelPair f a b → ∀ [CategoryTheory.IsIso a], CategoryTheory.Mono f
-- Mathlib.Data.Finsupp.Fin
Finsupp.cons_zero_single_eq_single_succ : ∀ {n : ℕ} (i : Fin n) {M : Type u_1} [inst : Zero M] (y : M), (Finsupp.cons 0 fun₀ | i => y) = fun₀ | i.succ => y
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.Quotient.eq_1 : ∀ {M : Type u_1} [inst : Add M] (c : AddCon M), c.Quotient = Quotient c.toSetoid
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.Monic.leadingCoeff_eq_one : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f : MvPolynomial σ R},
  m.Monic f → m.leadingCoeff f = 1
-- Std.Sat.AIG.CachedGatesLemmas
Std.Sat.AIG.denote_mkOrCached : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {assign : α → Bool} {aig : Std.Sat.AIG α}
  {input : aig.BinaryInput},
  ⟦assign, aig.mkOrCached input⟧ =
    (⟦assign, { aig := aig, ref := input.lhs }⟧ || ⟦assign, { aig := aig, ref := input.rhs }⟧)
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf
CategoryTheory.Sheaf.instHasExactLimitsOfShapeOfHasFiniteColimitsOfPreservesFiniteColimitsFunctorOppositeSheafToPresheaf : ∀ {C : Type u} {A : Type u₁} {K : Type u₂} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Category.{v₁, u₁} A] [inst_2 : CategoryTheory.Category.{v₂, u₂} K]
  (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.HasWeakSheafify J A]
  [CategoryTheory.Limits.HasFiniteColimits A] [inst_5 : CategoryTheory.Limits.HasLimitsOfShape K A]
  [CategoryTheory.HasExactLimitsOfShape K A]
  [CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.sheafToPresheaf J A)],
  CategoryTheory.HasExactLimitsOfShape K (CategoryTheory.Sheaf J A)
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
SSet.PtSimplex.RelStruct.refl_map : ∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} (f : X.PtSimplex n x) (i : Fin (n + 1)),
  (SSet.PtSimplex.RelStruct.refl f i).map = CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.σ i) f.map
-- Mathlib.NumberTheory.ZetaValues
intervalIntegrable_bernoulliFun : ∀ (k : ℕ) (a b : ℝ), IntervalIntegrable (bernoulliFun k) MeasureTheory.volume a b
-- Mathlib.CategoryTheory.Limits.Opposites
/-- Turn a limit of `F : J ⥤ Cᵒᵖ` into a colimit of `F.leftOp : Jᵒᵖ ⥤ C`.  -/
CategoryTheory.Limits.isColimitCoconeLeftOpOfCone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} J] →
        (F : CategoryTheory.Functor J Cᵒᵖ) →
          {c : CategoryTheory.Limits.Cone F} →
            CategoryTheory.Limits.IsLimit c →
              CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeLeftOpOfCone c)
-- Mathlib.MeasureTheory.Integral.Prod
/-- Double integrals commute with addition.  -/
MeasureTheory.integral_integral_add : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E] [MeasureTheory.SFinite ν]
  [inst_4 : NormedSpace ℝ E] [MeasureTheory.SFinite μ] ⦃f g : α × β → E⦄,
  MeasureTheory.Integrable f (μ.prod ν) →
    MeasureTheory.Integrable g (μ.prod ν) →
      ∫ (x : α), ∫ (y : β), f (x, y) + g (x, y) ∂ν ∂μ =
        ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ + ∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ
-- Mathlib.Order.Filter.Pointwise
Filter.pure_vsub_pure : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] {a b : β}, pure a -ᵥ pure b = pure (a -ᵥ b)
-- Mathlib.Analysis.Convex.Gauge
gauge_eq_one_iff_mem_frontier : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} {x : E} [inst_2 : TopologicalSpace E]
  [IsTopologicalAddGroup E] [ContinuousSMul ℝ E], Convex ℝ s → s ∈ nhds 0 → (gauge s x = 1 ↔ x ∈ frontier s)
-- Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi
/-- The equivalence `Karoubi C ≌ Karoubi (Karoubi C)`  -/
CategoryTheory.Idempotents.KaroubiKaroubi.equivalence : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.Idempotents.Karoubi C ≌ CategoryTheory.Idempotents.Karoubi (CategoryTheory.Idempotents.Karoubi C)
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.add.sizeOf_spec : ∀ (k : ℤ) (v : Int.Internal.Linear.Var) (p : Int.Internal.Linear.Poly),
  sizeOf (Int.Internal.Linear.Poly.add k v p) = 1 + sizeOf k + sizeOf v + sizeOf p
-- Mathlib.Topology.Homotopy.HSpaces
HSpace.prod : (X : Type u) →
  (Y : Type v) → [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → [HSpace X] → [HSpace Y] → HSpace (X × Y)
-- Mathlib.LinearAlgebra.TensorAlgebra.Grading
/-- A version of `TensorAlgebra.ι` that maps directly into the graded structure. This is
primarily an auxiliary construction used to provide `TensorAlgebra.gradedAlgebra`.  -/
TensorAlgebra.GradedAlgebra.ι : (R : Type u_1) →
  (M : Type u_2) →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → M →ₗ[R] DirectSum ℕ fun i => ↥((TensorAlgebra.ι R).range ^ i)
-- Mathlib.Data.Rat.Cast.Order
NNRat.cast_lt_natCast : ∀ {K : Type u_5} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] {m : ℚ≥0} {n : ℕ},
  ↑m < ↑n ↔ m < ↑n
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getThenInsertIfNew?!_fst : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] {k : α}
  {v : β}, (Std.DTreeMap.Internal.Impl.Const.getThenInsertIfNew?! t k v).1 = Std.DTreeMap.Internal.Impl.Const.get? t k
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
/-- If the angle between two vectors is π, the norm of their difference equals
the sum of their norms.  -/
InnerProductGeometry.norm_sub_eq_add_norm_of_angle_eq_pi : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  InnerProductGeometry.angle x y = Real.pi → ‖x - y‖ = ‖x‖ + ‖y‖
-- Mathlib.RingTheory.MatrixAlgebra
MatrixEquivTensor.invFun_smul : ∀ (n : Type u_3) (R : Type u_5) (A : Type u_7) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : DecidableEq n] [inst_4 : Fintype n] (a : A) (M : Matrix n n A),
  MatrixEquivTensor.invFun n R A (a • M) = a ⊗ₜ[R] 1 * MatrixEquivTensor.invFun n R A M
-- Mathlib.Condensed.Equivalence
Condensed.StoneanProfinite.instPreservesEffectiveEpisStoneanProfiniteToProfinite : Stonean.toProfinite.PreservesEffectiveEpis
-- Mathlib.CategoryTheory.Action.Limits
Action.neg_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.Preadditive V] {X Y : Action V G} (f : X ⟶ Y), (-f).hom = -f.hom
-- Mathlib.LinearAlgebra.QuadraticForm.Signature
le_sigPos_of_posDef : ∀ {R : Type u_1} {M : Type u_2} [inst : AddCommGroup M] [inst_1 : CommRing R] [inst_2 : LinearOrder R]
  [inst_3 : Module R M] (Q : QuadraticForm R M) [Module.Finite R M] [StrongRankCondition R] {V : Submodule R M},
  (QuadraticMap.restrict Q V).PosDef → Module.finrank R ↥V ≤ sigPos Q
-- Mathlib.MeasureTheory.Constructions.Pi
/-- We intentionally restrict this only to the nondependent function space, since
type-class inference cannot find an instance for `ι → ℝ` when this is stated for dependent function
spaces.  -/
MeasureTheory.Pi.isNegInvariant_volume : ∀ {ι : Type u_1} [inst : Fintype ι] {α : Type u_4} [inst_1 : AddGroup α] [inst_2 : MeasureTheory.MeasureSpace α]
  [MeasureTheory.SigmaFinite MeasureTheory.volume] [MeasurableNeg α] [MeasureTheory.volume.IsNegInvariant],
  MeasureTheory.volume.IsNegInvariant
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.log_opow_mul_add : ∀ {b u v w : Ordinal.{u_1}}, 1 < b → v ≠ 0 → w < b ^ u → Ordinal.log b (b ^ u * v + w) = u + Ordinal.log b v
-- Mathlib.Data.ENNReal.Real
ENNReal.toReal_ofReal_mul : ∀ (c : ℝ) (a : ENNReal), 0 ≤ c → (ENNReal.ofReal c * a).toReal = c * a.toReal
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the forward direction of `Asymptotics.isBigO_abs_left`. -/
Asymptotics.IsBigO.of_abs_left : ∀ {α : Type u_1} {F : Type u_4} [inst : Norm F] {g : α → F} {l : Filter α} {u : α → ℝ},
  (fun x => |u x|) =O[l] g → u =O[l] g
-- Mathlib.LinearAlgebra.Alternating.Basic
/-- Construct a linear equivalence between maps from a linear equivalence between domains.

This is `AlternatingMap.compLinearMap` as an isomorphism,
and the alternating version of `LinearEquiv.multilinearMapCongrLeft`.
It could also have been called `LinearEquiv.alternatingMapCongrLeft`.  -/
AlternatingMap.domLCongr : (R : Type u_1) →
  [inst : Semiring R] →
    {M : Type u_2} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          (N : Type u_3) →
            [inst_3 : AddCommMonoid N] →
              [inst_4 : Module R N] →
                (ι : Type u_7) →
                  {M₂ : Type u_10} →
                    [inst_5 : AddCommMonoid M₂] →
                      [inst_6 : Module R M₂] →
                        (S : Type u_12) →
                          [inst_7 : Semiring S] →
                            [inst_8 : Module S N] →
                              [inst_9 : SMulCommClass R S N] → (M ≃ₗ[R] M₂) → M [⋀^ι]→ₗ[R] N ≃ₗ[S] M₂ [⋀^ι]→ₗ[R] N
-- Init.Data.UInt.Lemmas
instCommutativeUInt32HMul : Std.Commutative fun x1 x2 => x1 * x2
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instAddMonoid : {m : Type u_1} → {n : Type u_2} → {A : Type u_5} → [AddMonoid A] → AddMonoid (CStarMatrix m n A)
-- Mathlib.NumberTheory.Dioph
/-- Diophantine sets are closed under intersection.  -/
Dioph.inter : ∀ {α : Type u} {S S' : Set (α → ℕ)}, Dioph S → Dioph S' → Dioph (S ∩ S')
-- Mathlib.Combinatorics.Additive.DoublingConst
/-- Dense sets have small doubling.  -/
Finset.addConst_le_inv_dens : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] {A B : Finset G} [inst_2 : Fintype G],
  A.addConst B ≤ A.dens⁻¹
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Functor.isEquivalence_trans : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [F.IsEquivalence] [G.IsEquivalence], (F.comp G).IsEquivalence
-- Mathlib.Analysis.Calculus.Rademacher
/-- A real-valued function on a finite-dimensional space which is Lipschitz is
differentiable almost everywhere. Superseded by
`LipschitzWith.ae_differentiableAt` which works for functions taking value in any
finite-dimensional space.  -/
LipschitzWith.ae_differentiableAt_of_real : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  {C : NNReal} {f : E → ℝ} {μ : MeasureTheory.Measure E} [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure],
  LipschitzWith C f → ∀ᵐ (x : E) ∂μ, DifferentiableAt ℝ f x
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.RightFraction.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} → {X Y X' : C} → (s : X' ⟶ X) → W s → (X' ⟶ Y) → W.RightFraction X Y
-- Mathlib.Algebra.Group.Subgroup.Pointwise
/-- The carrier of `N ⊔ H` is just `↑N * ↑H` (pointwise set product) when `N` is normal.  -/
Subgroup.normal_mul : ∀ {G : Type u_2} [inst : Group G] (N H : Subgroup G) [N.Normal], ↑(N ⊔ H) = ↑N * ↑H
-- Std.Sat.AIG.Basic
/-- Determine whether `ref` is a `Decl.const` with value `b`.
 -/
Std.Sat.AIG.isConstant : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → (aig : Std.Sat.AIG α) → aig.Ref → Bool → Bool
-- Mathlib.AlgebraicGeometry.Cover.Open
/-- Given any open cover `𝓤`, this is an affine open cover which refines it.  -/
AlgebraicGeometry.Scheme.OpenCover.fromAffineRefinement : {X : AlgebraicGeometry.Scheme} → (𝓤 : X.OpenCover) → 𝓤.affineRefinement.openCover ⟶ 𝓤
-- Mathlib.CategoryTheory.Bicategory.SingleObj
CategoryTheory.instInhabitedMonoidalSingleObj : (C : Type u_2) →
  [inst : CategoryTheory.Category.{u_1, u_2} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → Inhabited (CategoryTheory.MonoidalSingleObj C)
-- Mathlib.Condensed.Discrete.Colimit
Condensed.isColimitLocallyConstantPresheaf_desc_apply : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] [inst_1 : CategoryTheory.IsCofiltered I]
  {F : CategoryTheory.Functor I FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toProfinite))
  (X : Type (u + 1)) (hc : CategoryTheory.Limits.IsLimit c) [inst_2 : ∀ (i : I), CategoryTheory.Epi (c.π.app i)]
  (s : CategoryTheory.Limits.Cocone ((F.comp FintypeCat.toProfinite).op.comp (Condensed.locallyConstantPresheaf X)))
  (i : I) (f : LocallyConstant (↑(FintypeCat.toProfinite.obj (F.obj i)).toTop) X),
  (CategoryTheory.ConcreteCategory.hom ((Condensed.isColimitLocallyConstantPresheaf c X hc).desc s))
      (LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) f) =
    (CategoryTheory.ConcreteCategory.hom (s.ι.app (Opposite.op i))) f
-- Mathlib.Order.Bounds.Basic
IsGLB.mono : ∀ {α : Type u_1} [inst : Preorder α] {s t : Set α} {a b : α}, IsGLB s a → IsGLB t b → s ⊆ t → b ≤ a
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.reverse_mul : ∀ {R : Type u_1} [inst : Semiring R] {f g : Polynomial R},
  f.leadingCoeff * g.leadingCoeff ≠ 0 → (f * g).reverse = f.reverse * g.reverse
-- Lean.Widget.UserWidget
Lean.Widget.instFromJsonUserWidgetDefinition.fromJson : Lean.Json → Except String Lean.Widget.UserWidgetDefinition
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.Context.mk.injEq : ∀ (α : Lean.Expr) (univ : Lean.Level) (α0 : Lean.Expr) (isGroup : Bool) (inst α_1 : Lean.Expr) (univ_1 : Lean.Level)
  (α0_1 : Lean.Expr) (isGroup_1 : Bool) (inst_1 : Lean.Expr),
  ({ α := α, univ := univ, α0 := α0, isGroup := isGroup, inst := inst } =
      { α := α_1, univ := univ_1, α0 := α0_1, isGroup := isGroup_1, inst := inst_1 }) =
    (α = α_1 ∧ univ = univ_1 ∧ α0 = α0_1 ∧ isGroup = isGroup_1 ∧ inst = inst_1)
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
/-- Oplax associativity.  -/
CategoryTheory.OplaxFunctor.map₂_associator_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (self : CategoryTheory.OplaxFunctor B CategoryTheory.Cat)
  {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(self.obj a)),
  CategoryTheory.CategoryStruct.comp ((self.map₂ (CategoryTheory.Bicategory.associator f g h).hom).toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((self.mapComp f (CategoryTheory.CategoryStruct.comp g h)).toNatTrans.app X)
        ((self.mapComp g h).toNatTrans.app ((self.map f).toFunctor.obj X))) =
    CategoryTheory.CategoryStruct.comp ((self.mapComp (CategoryTheory.CategoryStruct.comp f g) h).toNatTrans.app X)
      ((self.map h).toFunctor.map ((self.mapComp f g).toNatTrans.app X))
-- Mathlib.Geometry.Manifold.GroupLieAlgebra
/-- The tangent space at the identity of an additive Lie group is a Lie algebra, for the bracket
given by the Lie bracket of invariant vector fields.  -/
instLieAlgebraAddGroupLieAlgebra : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {H : Type u_2} →
      [inst_1 : TopologicalSpace H] →
        {E : Type u_3} →
          [inst_2 : NormedAddCommGroup E] →
            [inst_3 : NormedSpace 𝕜 E] →
              {I : ModelWithCorners 𝕜 E H} →
                [inst_4 : CompleteSpace E] →
                  {G : Type u_5} →
                    [inst_5 : TopologicalSpace G] →
                      [inst_6 : ChartedSpace H G] →
                        [inst_7 : AddGroup G] →
                          [inst_8 : LieAddGroup I (minSmoothness 𝕜 3) G] → LieAlgebra 𝕜 (AddGroupLieAlgebra I G)
-- Init.Grind.Module.Basic
/-- Zero is the right identity for addition.  -/
Lean.Grind.AddCommMonoid.add_zero : ∀ {M : Type u} [self : Lean.Grind.AddCommMonoid M] (a : M), a + 0 = a
-- Mathlib.Algebra.BigOperators.Group.Finset.Gaps
Finset.prod_intervalGapsWithin_eq_div_div_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : CommGroup β] (F : Finset (α × α)) {k : ℕ}
  (h : F.card = k) {a b : α} (g : α → β),
  ∏ i ∈ Finset.range (k + 1), g (F.intervalGapsWithin h a b ↑i).2 / g (F.intervalGapsWithin h a b ↑i).1 =
    g b / g a / ∏ z ∈ F, g z.2 / g z.1
-- Init.Data.List.MinMaxOn
/-- Returns an element of `l` that minimizes `f`. If `x`, `y` are such that
`f x = f y`, it returns whichever comes first in the list. Returns `none` if the list is
empty.

The correctness of this function assumes `β` to be linearly pre-ordered.
The property that `List.minOn?` is the first minimizer in the list is guaranteed by the lemma
`List.getElem_get_minIdxOn?`
 -/
List.minOn? : {β : Type u_1} → {α : Type u_2} → [inst : LE β] → [DecidableLE β] → (α → β) → List α → Option α
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
/-- Map from `Lp F p (μ.trim hm)` to `lpMeasSubgroup`, inverse of
`lpMeasSubgroupToLpTrim`.  -/
MeasureTheory.lpTrimToLpMeasSubgroup : {α : Type u_1} →
  (F : Type u_2) →
    (p : ENNReal) →
      [inst : NormedAddCommGroup F] →
        {m m0 : MeasurableSpace α} →
          (μ : MeasureTheory.Measure α) →
            (hm : m ≤ m0) → ↥(MeasureTheory.Lp F p (μ.trim hm)) → ↥(MeasureTheory.lpMeasSubgroup F m p μ)
-- Init.Data.BitVec.Lemmas
BitVec.fill.eq_1 : ∀ (w : ℕ) (b : Bool), BitVec.fill w b = bif b then -1 else 0