mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- the compatibility condition on `fst` and `snd` with respect to the structure
isomorphisms  -/
CategoryTheory.Limits.CategoricalPullback.Hom.w_assoc : ∀ {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}
  {x y : CategoryTheory.Limits.CategoricalPullback F G} (self : x.Hom y) {Z : B} (h : G.obj y.snd ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map self.fst) (CategoryTheory.CategoryStruct.comp y.iso.hom h) =
    CategoryTheory.CategoryStruct.comp x.iso.hom (CategoryTheory.CategoryStruct.comp (G.map self.snd) h)
-- Mathlib.Algebra.Ring.Action.End
/-- The tautological action by the group of automorphism of a ring `R` on `R`.  -/
RingAut.applyMulSemiringAction : {R : Type u_2} → [inst : Semiring R] → MulSemiringAction (RingAut R) R
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.size_filter_eq_size_iff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α] {f : α → β → Bool},
  (↑m).WF →
    ((↑(Std.DHashMap.Internal.Raw₀.filter f m)).size = (↑m).size ↔
      ∀ (a : α) (h : m.contains a = true), f (m.getKey a h) (Std.DHashMap.Internal.Raw₀.Const.get m a h) = true)
-- Std.Http.Data.Version
/-- Converts a pair of `Nat` to the corresponding `Version`.
 -/
Std.Http.Version.ofNumber? : ℕ → ℕ → Option Std.Http.Version
-- Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
AlgebraicGeometry.WeaklyEtale.of_comp : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z)
  [AlgebraicGeometry.WeaklyEtale (CategoryTheory.CategoryStruct.comp f g)] [AlgebraicGeometry.WeaklyEtale g],
  AlgebraicGeometry.WeaklyEtale f
-- Mathlib.CategoryTheory.Limits.Filtered
CategoryTheory.Limits.hasLimitsOfShape_of_has_cofiltered_limits : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasCofilteredLimitsOfSize.{w', w, v, u} C] (I : Type w)
  [inst_2 : CategoryTheory.Category.{w', w} I] [CategoryTheory.IsCofiltered I],
  CategoryTheory.Limits.HasLimitsOfShape I C
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.image_toSnowflaking_ball : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : PseudoMetricSpace X] (x : X) {r : ℝ},
  0 ≤ r →
    ⇑Metric.Snowflaking.toSnowflaking '' Metric.ball x r = Metric.ball (Metric.Snowflaking.toSnowflaking x) (r ^ α)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- The product comparison morphism from `F(A ⨯ -)` to `FA ⨯ F-`, whose components are given by
`prodComparison`.
 -/
CategoryTheory.Limits.prodComparisonNatTrans : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{w, u₂} D] →
        [inst_2 : CategoryTheory.Limits.HasBinaryProducts C] →
          [inst_3 : CategoryTheory.Limits.HasBinaryProducts D] →
            (F : CategoryTheory.Functor C D) →
              (A : C) →
                (CategoryTheory.Limits.prod.functor.obj A).comp F ⟶
                  F.comp (CategoryTheory.Limits.prod.functor.obj (F.obj A))
-- Mathlib.Analysis.CStarAlgebra.ApproximateUnit
/-- The filter `CStarAlgebra.approximateUnit` generated by the sections
`{x | a ≤ x} ∩ closedBall 0 1` for `0 ≤ a` forms an increasing approximate unit.  -/
CStarAlgebra.increasingApproximateUnit : ∀ (A : Type u_1) [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : StarOrderedRing A],
  (CStarAlgebra.approximateUnit A).IsIncreasingApproximateUnit
-- Mathlib.Combinatorics.Schnirelmann
/-- The Schnirelmann density of any finite set is `0`.  -/
schnirelmannDensity_finite : ∀ {A : Set ℕ} [inst : DecidablePred fun x => x ∈ A], A.Finite → schnirelmannDensity A = 0
-- Mathlib.Order.Minimal
exists_maximal_ge_of_wellFoundedGT : ∀ {α : Type u_2} [inst : Preorder α] [WellFoundedGT α] (P : α → Prop) (a : α), P a → ∃ b, a ≤ b ∧ Maximal P b
-- Mathlib.NumberTheory.PrimeCounting
Nat.two_le_of_mem_primesLE : ∀ {p n : ℕ}, p ∈ n.primesLE → 2 ≤ p
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.map_X₄ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (sq : CategoryTheory.Square C) (F : CategoryTheory.Functor C D), (sq.map F).X₄ = F.obj sq.X₄
-- Std.Time.Notation
_private.Std.Time.Notation.0.Std.Time.convertPlainDate : Std.Time.PlainDate → Lean.MacroM (Lean.TSyntax `term)
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.get_slice : ∀ {s : String.Slice} {p p₀ p₁ : s.Pos} {h₁ : p₀ ≤ p} {h₂ : p ≤ p₁} {h : p.slice p₀ p₁ h₁ h₂ ≠ (s.slice p₀ p₁ ⋯).endPos},
  (p.slice p₀ p₁ h₁ h₂).get h = p.get ⋯
-- Mathlib.CategoryTheory.Monoidal.Category
/-- Tensoring on the left, as a functor from `C` into endofunctors of `C`.

TODO: show this is an op-monoidal functor.
 -/
CategoryTheory.MonoidalCategory.tensoringLeft : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.MonoidalCategory C] → CategoryTheory.Functor C (CategoryTheory.Functor C C)
-- Mathlib.Algebra.Group.Commute.Defs
Commute.one_right : ∀ {M : Type u_2} [inst : MulOneClass M] (a : M), Commute a 1
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.mapIso_functor_map_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T T' : D} {S : CategoryTheory.Functor C D} (i : T ≅ T')
  {Y X : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)} (f : Y ⟶ X),
  ((CategoryTheory.CostructuredArrow.mapIso i).functor.map f).left = f.left
-- Lean.Compiler.IR.Basic
Lean.IR.LocalContextEntry : Type
-- Mathlib.Data.Fintype.Perm
mem_permsOfList_iff : ∀ {α : Type u_1} [inst : DecidableEq α] {l : List α} {f : Equiv.Perm α}, f ∈ permsOfList l ↔ ∀ {x : α}, f x ≠ x → x ∈ l
-- Mathlib.Geometry.Convex.Hull
Convexity.IsConvexSet.convexHull : ∀ {R : Type u_1} {X : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X] {s : Set X}, Convexity.IsConvexSet R ((Convexity.convexHull R) s)
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
/-- The action of the alternating group has trivial blocks.

This holds for any `α`, even when `Nat.card α ≤ 2` and the action
is not preprimitive, because it is not pretransitive.  -/
alternatingGroup.isTrivialBlock_of_isBlock : ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : DecidableEq α] {B : Set α},
  MulAction.IsBlock (↥(alternatingGroup α)) B → MulAction.IsTrivialBlock B
-- Std.Time.Format.Modifier
/-- `classifyNumberText` classifies the number of pattern letters into either a `Number` or `Text`.
 -/
Std.Time.classifyNumberText : ℕ → Option (Std.Time.Number ⊕ Std.Time.Text)
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.mapAlgHom_id : ∀ {R : Type u} {A : Type z} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  Polynomial.mapAlgHom (AlgHom.id R A) = AlgHom.id R (Polynomial A)
-- Mathlib.GroupTheory.Torsion
/-- The torsion submonoid of an abelian group equals the torsion subgroup as a submonoid.  -/
CommGroup.torsion_eq_torsion_submonoid : ∀ (G : Type u_1) [inst : CommGroup G], CommMonoid.torsion G = (CommGroup.torsion G).toSubmonoid
-- Mathlib.Data.List.MinMax
List.not_lt_of_mem_argmin : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] [inst_1 : DecidableLT β] {f : α → β} {l : List α} {a m : α},
  a ∈ l → m ∈ List.argmin f l → ¬f a < f m
-- Aesop.Stats.Basic
Aesop.RuleStats.mk.inj : ∀ {rule : Aesop.DisplayRuleName} {elapsed : Aesop.Nanos} {successful : Bool} {rule_1 : Aesop.DisplayRuleName}
  {elapsed_1 : Aesop.Nanos} {successful_1 : Bool},
  { rule := rule, elapsed := elapsed, successful := successful } =
      { rule := rule_1, elapsed := elapsed_1, successful := successful_1 } →
    rule = rule_1 ∧ elapsed = elapsed_1 ∧ successful = successful_1
-- Mathlib.Analysis.MeanInequalities
Real.geom_mean_lt_arith_mean2_weighted_iff_of_pos : ∀ {w₁ w₂ p₁ p₂ : ℝ}, 0 < w₁ → 0 < w₂ → 0 ≤ p₁ → 0 ≤ p₂ → w₁ + w₂ = 1 → (p₁ ^ w₁ * p₂ ^ w₂ < w₁ * p₁ + w₂ * p₂ ↔ p₁ ≠ p₂)
-- Mathlib.RingTheory.Extension.Presentation.Submersive
/-- If `σ` has a `Fintype` and `DecidableEq` instance, the differential of `P`
can be expressed in matrix form.
 -/
Algebra.PreSubmersivePresentation.jacobiMatrix : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      {σ : Type t} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              (P : Algebra.PreSubmersivePresentation R S ι σ) → [Fintype σ] → [DecidableEq σ] → Matrix σ σ P.Ring
-- Mathlib.SetTheory.Ordinal.Principal
/-- The main characterization theorem for multiplicative principal ordinals.  -/
Ordinal.isPrincipal_mul_iff_le_two_or_omega0_opow_opow : ∀ {o : Ordinal.{u}},
  Ordinal.IsPrincipal (fun x1 x2 => x1 * x2) o ↔ o ≤ 2 ∨ o ∈ Set.range fun x => Ordinal.omega0 ^ Ordinal.omega0 ^ x
-- Lean.Parser.Basic
/-- Parses characters after the first `"`. If we need to start counting `#`'s to decide if we are closing
the raw string literal, we switch to `closingState`.
 -/
_private.Lean.Parser.Basic.0.Lean.Parser.rawStrLitFnAux.normalState : String.Pos.Raw → ℕ → Lean.Parser.ParserContext → Lean.Parser.ParserState → Lean.Parser.ParserState
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.erase_sub : ∀ {ι : Type u} [inst : DecidableEq ι] {β : ι → Type v} [inst_1 : (i : ι) → AddGroup (β i)] (i : ι)
  (f g : Π₀ (i : ι), β i), DFinsupp.erase i (f - g) = DFinsupp.erase i f - DFinsupp.erase i g
-- Mathlib.CategoryTheory.SmallRepresentatives
CategoryTheory.CoreSmallCategoryOfSet.functor_obj : ∀ {Ω : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (h : CategoryTheory.CoreSmallCategoryOfSet Ω C)
  (a : ↑h.obj), h.functor.obj a = h.objEquiv a
-- Mathlib.GroupTheory.Finiteness
AddSubmonoid.FG.map_injective : ∀ {M : Type u_1} [inst : AddMonoid M] {M' : Type u_3} [inst_1 : AddMonoid M'] {P : AddSubmonoid M} (e : M →+ M'),
  Function.Injective ⇑e → (AddSubmonoid.map e P).FG → P.FG
-- Mathlib.Algebra.Lie.Basis.Prod
_private.Mathlib.Algebra.Lie.Basis.Prod.0.LieAlgebra.Basis.basisProd_aux : ∀ {ι₁ : Type u_1} {ι₂ : Type u_2} {L₁ : Type u_3} {L₂ : Type u_4} [inst : Finite ι₁] [inst_1 : Finite ι₂] (eι : ι₁ ≃ ι₂)
  [inst_2 : LieRing L₁] [inst_3 : LieRing L₂] {R : Type u_5} [inst_4 : CommRing R] [inst_5 : LieAlgebra R L₁]
  {H₁ : LieSubalgebra R L₁} (b₁ : LieAlgebra.Basis ι₁ H₁) [inst_6 : LieAlgebra R L₂] {H₂ : LieSubalgebra R L₂}
  (b₂ : LieAlgebra.Basis ι₂ H₂),
  LieSubalgebra.lieSpan R (↥(LieAlgebra.Basis.prod✝ eι b₁ b₂))
      (Set.range (LieAlgebra.Basis.prodE✝ eι b₁ b₂) ∪ Set.range (LieAlgebra.Basis.prodF✝ eι b₁ b₂)) =
    ⊤
-- Mathlib.MeasureTheory.Measure.Support
MeasureTheory.Measure.support_mono : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] {μ ν : MeasureTheory.Measure X},
  μ ≤ ν → μ.support ⊆ ν.support
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
UniqueFactorizationMonoid.irreducible_of_normalized_factor : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizationMonoid α] [inst_2 : UniqueFactorizationMonoid α]
  {a : α}, ∀ x ∈ UniqueFactorizationMonoid.normalizedFactors a, Irreducible x
-- Mathlib.RingTheory.Polynomial.Basic
/-- A stronger version of `Polynomial.exists_degree_le_of_mem_span` under the assumption that the
set `s : R[X]` is finite. There exists a polynomial `p' ∈ s` whose degree dominates the degree of
every element of `p ∈ span R s`.  -/
Polynomial.exists_degree_le_of_mem_span_of_finite : ∀ {R : Type u} [inst : Semiring R] {s : Set (Polynomial R)},
  s.Finite → s.Nonempty → ∃ p' ∈ s, ∀ p ∈ Submodule.span R s, p.degree ≤ p'.degree
-- Std.Internal.Do.ExceptPost
/-- Pretty-print `EPost.Cons` as `EPost⟨e₁, e₂, ...⟩`.  -/
Std.Internal.Do.unexpandEPostCons : Lean.PrettyPrinter.Unexpander
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubmonoid.neg_val_mem_of_mem_addUnits : ∀ {M : Type u_1} [inst : AddMonoid M] (S : AddSubmonoid M) {x : AddUnits M}, x ∈ S.addUnits → ↑(-x) ∈ S
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.eq_const : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [PreconnectedSpace X] (f : LocallyConstant X Y) (x : X),
  f = LocallyConstant.const X (f x)
-- Mathlib.GroupTheory.CommutingProbability
DihedralGroup.reciprocalFactors.eq_1 : ∀ (n : ℕ),
  DihedralGroup.reciprocalFactors n =
    if x : n = 0 then [0]
    else
      if x : n = 1 then []
      else
        if Even n then 3 :: DihedralGroup.reciprocalFactors (n / 2)
        else n % 4 * n :: DihedralGroup.reciprocalFactors (n / 4 + 1)
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
/-- Given `f, g : X ⟶ Spec(R)`, if the two induced maps `R ⟶ Γ(X)` are equal, then `f = g`.  -/
AlgebraicGeometry.ext_to_Spec : ∀ {X : AlgebraicGeometry.Scheme} {R : Type u_1} [inst : CommRing R]
  {f g : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of R)},
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso (CommRingCat.of R)).inv
        (AlgebraicGeometry.Scheme.Γ.map f.op) =
      CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso (CommRingCat.of R)).inv
        (AlgebraicGeometry.Scheme.Γ.map g.op) →
    f = g
-- Lean.Meta.WHNF
_private.Lean.Meta.WHNF.0.Lean.Meta.whnfMatcher : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.Limits.Types.Pullbacks
/-- The explicit pullback cone on `PullbackObj f g`.
This is bundled with the `IsLimit` data as `pullbackLimitCone f g`.
 -/
CategoryTheory.Limits.Types.pullbackCone : {X Y Z : Type u} → (f : X ⟶ Z) → (g : Y ⟶ Z) → CategoryTheory.Limits.PullbackCone f g
-- Mathlib.Topology.Order.LiminfLimsup
/-- The `liminf` of a function `u` along a filter `f` is the least cluster point of `u` along
`f`.  -/
isLeast_mapClusterPt_liminf : ∀ {α : Type u_2} {β : Type u_3} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
  [OrderTopology α] {u : β → α} {f : Filter β} [f.NeBot],
  autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f u) isLeast_mapClusterPt_liminf._auto_1 →
    autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) isLeast_mapClusterPt_liminf._auto_3 →
      IsLeast {x | MapClusterPt x f u} (Filter.liminf u f)
-- Mathlib.Combinatorics.Matroid.Sum
Matroid.disjointSigma.eq_1 : ∀ {α : Type u_1} {ι : Type u_2} (M : ι → Matroid α) (h : Pairwise (Function.onFun Disjoint fun i => (M i).E)),
  Matroid.disjointSigma M h =
    (Matroid.sigma fun i => (M i).restrictSubtype (M i).E).mapEmbedding (Function.Embedding.sigmaSet h)
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.mapConeEquiv.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] {K : CategoryTheory.Functor J C}
  {F G : CategoryTheory.Functor C D} (h : F ≅ G) {c : CategoryTheory.Limits.Cone K}
  (t : CategoryTheory.Limits.IsLimit (F.mapCone c)),
  CategoryTheory.Limits.IsLimit.mapConeEquiv h t =
    (CategoryTheory.Limits.IsLimit.postcomposeInvEquiv (K.isoWhiskerLeft h) (G.mapCone c))
      (t.ofIsoLimit (CategoryTheory.Functor.postcomposeWhiskerLeftMapCone h.symm c).symm)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.insertMany_cons : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {l : List (α × β)} {k : α} {v : β}, t.insertMany ((k, v) :: l) = (t.insert k v).insertMany l
-- Mathlib.Order.Filter.Map
Filter.map_inf : ∀ {α : Type u_1} {β : Type u_2} {f g : Filter α} {m : α → β},
  Function.Injective m → Filter.map m (f ⊓ g) = Filter.map m f ⊓ Filter.map m g
-- Mathlib.Combinatorics.Additive.Energy
Finset.addEnergy_empty_right : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Add α] (s : Finset α), s.addEnergy ∅ = 0
-- Std.Data.HashSet.Lemmas
Std.HashSet.Equiv.union_congr : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ m₃ m₄ : Std.HashSet α} [EquivBEq α] [LawfulHashable α],
  m₁.Equiv m₃ → m₂.Equiv m₄ → (m₁ ∪ m₂).Equiv (m₃ ∪ m₄)
-- Lean.Server.InfoUtils
Lean.Elab.InfoTree.getCompletionInfos : Lean.Elab.InfoTree → Array (Lean.Elab.ContextInfo × Lean.Elab.CompletionInfo)
-- Mathlib.Order.Interval.Basic
NonemptyInterval.coe_nonempty : ∀ {α : Type u_1} [inst : Preorder α] (s : NonemptyInterval α), (Set.Icc s.toProd.1 s.toProd.2).Nonempty
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.size_filter_le_size : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {f : (a : α) → β a → Bool}, t.WF → (Std.DTreeMap.Raw.filter f t).size ≤ t.size
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.shiftFunctorZero'.eq_1 : ∀ (C : Type u) {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (a : A) (ha : a = 0),
  CategoryTheory.shiftFunctorZero' C a ha = CategoryTheory.eqToIso ⋯ ≪≫ CategoryTheory.shiftFunctorZero C A
-- Init.Data.Format.Basic
_private.Init.Data.Format.Basic.0.Std.Format.WorkItem.mk.inj : ∀ {f : Std.Format} {indent : ℤ} {activeTags : ℕ} {f_1 : Std.Format} {indent_1 : ℤ} {activeTags_1 : ℕ},
  { f := f, indent := indent, activeTags := activeTags } =
      { f := f_1, indent := indent_1, activeTags := activeTags_1 } →
    f = f_1 ∧ indent = indent_1 ∧ activeTags = activeTags_1
-- Mathlib.Order.Partition.Basic
Partition.mk.injEq : ∀ {α : Type u_1} [inst : CompleteLattice α] {s : α} (parts : Set α) (sSupIndep' : sSupIndep parts)
  (bot_notMem' : ⊥ ∉ parts) (sSup_eq' : sSup parts = s) (parts_1 : Set α) (sSupIndep'_1 : sSupIndep parts_1)
  (bot_notMem'_1 : ⊥ ∉ parts_1) (sSup_eq'_1 : sSup parts_1 = s),
  ({ parts := parts, sSupIndep' := sSupIndep', bot_notMem' := bot_notMem', sSup_eq' := sSup_eq' } =
      { parts := parts_1, sSupIndep' := sSupIndep'_1, bot_notMem' := bot_notMem'_1, sSup_eq' := sSup_eq'_1 }) =
    (parts = parts_1)
-- Mathlib.Topology.FiberBundle.Basic
FiberPrebundle.mk.inj : ∀ {B : Type u_2} {F : Type u_3} {E : B → Type u_5} {inst : TopologicalSpace B} {inst_1 : TopologicalSpace F}
  {inst_2 : (x : B) → TopologicalSpace (E x)}
  {pretrivializationAtlas : Set (Bundle.Pretrivialization F Bundle.TotalSpace.proj)}
  {pretrivializationAt : B → Bundle.Pretrivialization F Bundle.TotalSpace.proj}
  {mem_base_pretrivializationAt : ∀ (x : B), x ∈ (pretrivializationAt x).baseSet}
  {pretrivialization_mem_atlas : ∀ (x : B), pretrivializationAt x ∈ pretrivializationAtlas}
  {continuous_trivChange :
    ∀ e ∈ pretrivializationAtlas,
      ∀ e' ∈ pretrivializationAtlas, ContinuousOn (↑e ∘ ↑e'.symm) (e'.target ∩ ↑e'.symm ⁻¹' e.source)}
  {totalSpaceMk_isInducing : ∀ (b : B), Topology.IsInducing (↑(pretrivializationAt b) ∘ Bundle.TotalSpace.mk b)}
  {pretrivializationAtlas_1 : Set (Bundle.Pretrivialization F Bundle.TotalSpace.proj)}
  {pretrivializationAt_1 : B → Bundle.Pretrivialization F Bundle.TotalSpace.proj}
  {mem_base_pretrivializationAt_1 : ∀ (x : B), x ∈ (pretrivializationAt_1 x).baseSet}
  {pretrivialization_mem_atlas_1 : ∀ (x : B), pretrivializationAt_1 x ∈ pretrivializationAtlas_1}
  {continuous_trivChange_1 :
    ∀ e ∈ pretrivializationAtlas_1,
      ∀ e' ∈ pretrivializationAtlas_1, ContinuousOn (↑e ∘ ↑e'.symm) (e'.target ∩ ↑e'.symm ⁻¹' e.source)}
  {totalSpaceMk_isInducing_1 : ∀ (b : B), Topology.IsInducing (↑(pretrivializationAt_1 b) ∘ Bundle.TotalSpace.mk b)},
  { pretrivializationAtlas := pretrivializationAtlas, pretrivializationAt := pretrivializationAt,
        mem_base_pretrivializationAt := mem_base_pretrivializationAt,
        pretrivialization_mem_atlas := pretrivialization_mem_atlas, continuous_trivChange := continuous_trivChange,
        totalSpaceMk_isInducing := totalSpaceMk_isInducing } =
      { pretrivializationAtlas := pretrivializationAtlas_1, pretrivializationAt := pretrivializationAt_1,
        mem_base_pretrivializationAt := mem_base_pretrivializationAt_1,
        pretrivialization_mem_atlas := pretrivialization_mem_atlas_1, continuous_trivChange := continuous_trivChange_1,
        totalSpaceMk_isInducing := totalSpaceMk_isInducing_1 } →
    pretrivializationAtlas = pretrivializationAtlas_1 ∧ pretrivializationAt = pretrivializationAt_1
-- Mathlib.Analysis.Complex.Norm
Complex.nnnorm_nnratCast : ∀ (q : ℚ≥0), ‖↑q‖₊ = ↑q
-- Mathlib.MeasureTheory.Group.FoelnerFilter
isAddFoelner_iff_tendsto : ∀ {G : Type u_1} {X : Type u_2} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : AddGroup G]
  [inst_2 : AddAction G X] {ι : Type u_3} (l : Filter ι) (F : ι → Set X),
  IsAddFoelner G μ l F ↔ Filter.Tendsto F l (maxAddFoelner G μ)
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
/-- `PComp.scale c n` scales the coefficients of `c` by `n` and notes this in the `CompSource`.  -/
Mathlib.Tactic.Linarith.PComp.scale : Mathlib.Tactic.Linarith.PComp → ℕ → Mathlib.Tactic.Linarith.PComp
-- Mathlib.Algebra.Homology.Embedding.TruncGE
/-- The isomorphism `(K.truncGE e).X i' ≅ K.X i'` when `e.f i = i'`
and `e.BoundaryGE i` does not hold.  -/
HomologicalComplex.truncGEXIso : {ι : 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.HasZeroMorphisms C] →
              (K : HomologicalComplex C c') →
                (e : c.Embedding c') →
                  [inst_2 : e.IsTruncGE] →
                    [inst_3 : ∀ (i' : ι'), K.HasHomology i'] →
                      [inst_4 : CategoryTheory.Limits.HasZeroObject C] →
                        {i : ι} → {i' : ι'} → e.f i = i' → ¬e.BoundaryGE i → ((K.truncGE e).X i' ≅ K.X i')
-- Init.Data.Nat.Lemmas
Nat.zero_pow : ∀ {n : ℕ}, 0 < n → 0 ^ n = 0
-- Mathlib.Analysis.Convex.Jensen
/-- Concave **Jensen's inequality**, `Finset.centerMass` version.  -/
ConcaveOn.le_map_centerMass : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜]
  [IsStrictOrderedRing 𝕜] [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup β] [inst_5 : PartialOrder β]
  [IsOrderedAddMonoid β] [inst_7 : Module 𝕜 E] [inst_8 : Module 𝕜 β] [IsStrictOrderedModule 𝕜 β] {s : Set E} {f : E → β}
  {t : Finset ι} {w : ι → 𝕜} {p : ι → E},
  ConcaveOn 𝕜 s f →
    (∀ i ∈ t, 0 ≤ w i) → 0 < ∑ i ∈ t, w i → (∀ i ∈ t, p i ∈ s) → t.centerMass w (f ∘ p) ≤ f (t.centerMass w p)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
/-- `CFC.sqrt` is operator monotone.  -/
CFC.monotone_sqrt : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : StarOrderedRing A],
  Monotone CFC.sqrt
-- Mathlib.Order.Basic
le_of_forall_gt_imp_ge_of_dense : ∀ {α : Type u_2} [inst : LinearOrder α] [DenselyOrdered α] {a₁ a₂ : α}, (∀ (a : α), a₂ < a → a₁ ≤ a) → a₁ ≤ a₂
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Complex.tan_add_mul_I : ∀ {x y : ℂ},
  (((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * ↑Real.pi / 2) ∧ ∀ (l : ℤ), y * Complex.I ≠ (2 * ↑l + 1) * ↑Real.pi / 2) ∨
      (∃ k, x = (2 * ↑k + 1) * ↑Real.pi / 2) ∧ ∃ l, y * Complex.I = (2 * ↑l + 1) * ↑Real.pi / 2) →
    Complex.tan (x + y * Complex.I) =
      (Complex.tan x + Complex.tanh y * Complex.I) / (1 - Complex.tan x * Complex.tanh y * Complex.I)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get_min : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {he : t.isEmpty = false}
  {hc : t.min he ∈ t}, t.get (t.min he) hc = t.min he
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- Given a localization map `f : M →+ N` for a submonoid `S ⊆ M` and a map of
`AddCommMonoid`s `g : M →+ P` such that `g y` is invertible for all `y : S`, the homomorphism
induced from `N` to `P` sending `z : N` to `g x - g y`, where `(x, y) : M × S` are such that
`z = f x - f y`.  -/
AddSubmonoid.LocalizationMap.lift : {M : Type u_1} →
  [inst : AddCommMonoid M] →
    {S : AddSubmonoid M} →
      {N : Type u_2} →
        [inst_1 : AddCommMonoid N] →
          {P : Type u_3} →
            [inst_2 : AddCommMonoid P] → S.LocalizationMap N → {g : M →+ P} → (∀ (y : ↥S), IsAddUnit (g ↑y)) → N →+ P