mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Int.Linear
Int.Internal.Linear.eq_def_norm : ∀ (ctx : Int.Internal.Linear.Context) (x : Int.Internal.Linear.Var) (xPoly xPoly' p : Int.Internal.Linear.Poly),
  Int.Internal.Linear.eq_def_cert x xPoly' p = true →
    Int.Internal.Linear.Var.denote ctx x = Int.Internal.Linear.Poly.denote' ctx xPoly →
      Int.Internal.Linear.Poly.denote' ctx xPoly = Int.Internal.Linear.Poly.denote' ctx xPoly' →
        Int.Internal.Linear.Poly.denote' ctx p = 0
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.π_truncGTIsoTruncGE_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b),
  CategoryTheory.CategoryStruct.comp (t.truncGTπ a) (t.truncGTIsoTruncGE a b h).hom = t.truncGEπ b
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.ofAbs_toAbs : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Semiring R]
  (v : AbsoluteValue R S) (x : R), (WithAbs.toAbs v x).ofAbs = x
-- Std.Data.Iterators.Lemmas.Equivalence.Basic
_private.Std.Data.Iterators.Lemmas.Equivalence.Basic.0.Std.quotMk_quot_eq_quot_eq_quotOfQuot_comp : ∀ {α : Sort u_1} (R : α → α → Prop), (Quot.mk fun x1 x2 => Quot.mk R x1 = Quot.mk R x2) = Std.quotOfQuot✝ ⋯ ∘ Quot.mk R
-- Init.Data.List.Zip
List.zip_eq_zipWith : ∀ {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List β}, l₁.zip l₂ = List.zipWith Prod.mk l₁ l₂
-- Mathlib.CategoryTheory.ConcreteCategory.EpiMono
CategoryTheory.ConcreteCategory.epi_iff_surjective_of_preservesPushout : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {X Y : C}
  (f : X ⟶ Y)
  [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingSpan (CategoryTheory.forget C)],
  CategoryTheory.Epi f ↔ Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Init.Data.String.Basic
String.rawEndPos_sliceTo : ∀ {s : String} {p : s.Pos}, (s.sliceTo p).rawEndPos = p.offset
-- Init.Data.Nat.Lemmas
Nat.mul_left_cancel_iff : ∀ {n : ℕ}, 0 < n → ∀ {m k : ℕ}, n * m = n * k ↔ m = k
-- Lean.Server.RequestCancellation
Lean.Server.RequestCancellationToken.cancelledByCancelRequest : Lean.Server.RequestCancellationToken → IO.CancelToken
-- Mathlib.CategoryTheory.Limits.Presentation
CategoryTheory.Limits.ColimitPresentation.changeDiag_diag : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.Category.{t, w} J]
  {X : C} (P : CategoryTheory.Limits.ColimitPresentation J X) {F : CategoryTheory.Functor J C} (e : F ≅ P.diag),
  (P.changeDiag e).diag = F
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.IsSt.mul : ∀ {x y : ℝ*} {r s : ℝ}, x.IsSt r → y.IsSt s → (x * y).IsSt (r * s)
-- Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC
/-- If a point of `Spec R[x]` is not contained in the vanishing set of `f`, then its image in
`Spec R` is contained in the open set where at least one of the coefficients of `f` is non-zero.
This lemma is a reformulation of `exists_C_coeff_notMem`.  -/
AlgebraicGeometry.Polynomial.comap_C_mem_imageOfDf : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R} {I : PrimeSpectrum (Polynomial R)},
  I ∈ (PrimeSpectrum.zeroLocus {f})ᶜ → PrimeSpectrum.comap Polynomial.C I ∈ AlgebraicGeometry.Polynomial.imageOfDf f
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.add_lt_add_left : ∀ {α : Type u} [inst : Add α] {x y z : WithBot α} [inst_1 : LT α] [AddLeftStrictMono α], x ≠ ⊥ → y < z → x + y < x + z
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.op_isomorphisms : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  (CategoryTheory.MorphismProperty.isomorphisms C).op = CategoryTheory.MorphismProperty.isomorphisms Cᵒᵖ
-- Mathlib.Algebra.Order.Group.Opposite
AddOpposite.op_le_one : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : PartialOrder α] {a : α}, AddOpposite.op a ≤ 1 ↔ a ≤ 1
-- Mathlib.Tactic.Push
/-- `push c` rewrites the goal by pushing the constant `c` deeper into an expression.
For instance, `push _ ∈ _` rewrites `x ∈ {y} ∪ zᶜ` into `x = y ∨ ¬ x ∈ z`.
More precisely, the `push` tactic repeatedly rewrites an expression by applying lemmas
of the form `c ... = ... (c ...)` (where `c` can appear 0 or more times on the right hand side).
To extend the `push` tactic, you can tag a lemma of this form with the `@[push]` attribute.

To instead move a constant closer to the head of the expression, use the `pull` tactic.

`push` works as both a tactic and a conv tactic.

* `push _ ~ _` pushes the (binary) operator `~`, `push ~ _` pushes the (unary) operator `~`.
* `push c at l1 l2 ...` rewrites at the given locations.
* `push c at *` rewrites at all hypotheses and the goal.
* `push +distrib Not` rewrites `¬ (p ∧ q)` into `¬ p ∨ ¬ q` (without `+distrib`, it rewrites it
  into `p → ¬ q` instead).
* `push (disch := tac) c` uses the tactic `tac` to discharge any hypotheses for `@[push]` lemmas.

Examples:
* `push Not` is the same as `push ¬ _`, and it rewrites `¬ ∀ ε > 0, ∃ δ > 0, δ < ε` into
  `∃ ε > 0, ∀ δ > 0, ε ≤ δ`. Notably, this preserves the binder names.
* `push _ ∈ _` rewrites `x ∈ {y} ∪ zᶜ` into `x = y ∨ ¬ x ∈ z`.
* `push (disch := positivity) Real.log` rewrites `log (a * b ^ 2)` into `log a + 2 * log b`.
* `push fun _ ↦ _` rewrites `fun x => f x ^ 2 + 5` into `f ^ 2 + 5`
* `push ∀ _, _` rewrites `∀ a, p a ∧ q a` into `(∀ a, p a) ∧ (∀ a, q a)`.
 -/
Mathlib.Tactic.Push.pushStx : Lean.ParserDescr
-- Mathlib.Data.WSeq.Relation
/-- If two sequences are equivalent, then they have the same values and
the same computational behavior (i.e. if one loops forever then so does
the other), although they may differ in the number of `think`s needed to
arrive at the answer.  -/
Stream'.WSeq.«term_~ʷ_» : Lean.TrailingParserDescr
-- Init.Grind.Module.Envelope
Lean.Grind.IntModule.OfNatModule.sub_eq_add_neg : ∀ {α : Type u} [inst : Lean.Grind.NatModule α] (a b : Lean.Grind.IntModule.OfNatModule.Q α),
  Lean.Grind.IntModule.OfNatModule.sub a b =
    Lean.Grind.IntModule.OfNatModule.add a (Lean.Grind.IntModule.OfNatModule.neg b)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getD_inter_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α} {fallback : β}, k ∉ m₁ → Std.DHashMap.Const.getD (m₁.inter m₂) k fallback = fallback
-- Mathlib.Data.Set.Function
Set.SurjOn.of_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {p : Set γ} {f : α → β} {g : β → γ},
  Set.SurjOn (g ∘ f) s p → Set.MapsTo f s t → Set.SurjOn g t p
-- Mathlib.CategoryTheory.FiberedCategory.Grothendieck
CategoryTheory.Pseudofunctor.CoGrothendieck.ι_obj_base : ∀ {𝒮 : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} 𝒮]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat) (S : 𝒮)
  (a : ↑(F.obj { as := Opposite.op S })), ((CategoryTheory.Pseudofunctor.CoGrothendieck.ι F S).obj a).base = S
-- Lean.Meta.AbstractMVars
Lean.Meta.AbstractMVars.State.mk.inj : ∀ {ngen : Lean.NameGenerator} {lctx : Lean.LocalContext} {mctx : Lean.MetavarContext} {nextParamIdx : ℕ}
  {paramNames : Array Lean.Name} {fvars mvars : Array Lean.Expr} {lmap : Std.HashMap Lean.LMVarId Lean.Level}
  {emap : Std.HashMap Lean.MVarId Lean.Expr} {abstractLevels : Bool} {ngen_1 : Lean.NameGenerator}
  {lctx_1 : Lean.LocalContext} {mctx_1 : Lean.MetavarContext} {nextParamIdx_1 : ℕ} {paramNames_1 : Array Lean.Name}
  {fvars_1 mvars_1 : Array Lean.Expr} {lmap_1 : Std.HashMap Lean.LMVarId Lean.Level}
  {emap_1 : Std.HashMap Lean.MVarId Lean.Expr} {abstractLevels_1 : Bool},
  { ngen := ngen, lctx := lctx, mctx := mctx, nextParamIdx := nextParamIdx, paramNames := paramNames, fvars := fvars,
        mvars := mvars, lmap := lmap, emap := emap, abstractLevels := abstractLevels } =
      { ngen := ngen_1, lctx := lctx_1, mctx := mctx_1, nextParamIdx := nextParamIdx_1, paramNames := paramNames_1,
        fvars := fvars_1, mvars := mvars_1, lmap := lmap_1, emap := emap_1, abstractLevels := abstractLevels_1 } →
    ngen = ngen_1 ∧
      lctx = lctx_1 ∧
        mctx = mctx_1 ∧
          nextParamIdx = nextParamIdx_1 ∧
            paramNames = paramNames_1 ∧
              fvars = fvars_1 ∧ mvars = mvars_1 ∧ lmap = lmap_1 ∧ emap = emap_1 ∧ abstractLevels = abstractLevels_1
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.Grothendieck.mk.sizeOf_spec : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} [inst_1 : SizeOf 𝒮]
  (base : 𝒮) (fiber : ↑(F.obj { as := base })), sizeOf { base := base, fiber := fiber } = 1 + sizeOf base + sizeOf fiber
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_sum_of_countable : ∀ {α : Type u_2} {ι : Type u_6} {m0 : MeasurableSpace α} [Countable ι] (μ : ι → MeasureTheory.Measure α) (s : Set α),
  (MeasureTheory.Measure.sum μ).restrict s = MeasureTheory.Measure.sum fun i => (μ i).restrict s
-- Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric
_private.Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric.0.integral_log_sin_zero_pi_eq_two_mul_integral_log_sin_zero_pi_div_two : ∫ (x : ℝ) in 0..Real.pi, Real.log (Real.sin x) = 2 * ∫ (x : ℝ) in 0..Real.pi / 2, Real.log (Real.sin x)
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Embedding.refl_comp : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ↪g G'),
  SimpleGraph.Embedding.refl.comp f = f
-- Mathlib.Order.SymmDiff
le_bihimp_inf_right : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] (a b : α), bihimp a b ⊓ b ≤ a
-- Init.Data.List.MapIdx
List.mapFinIdx_eq_nil_iff : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : (i : ℕ) → α → i < l.length → β}, l.mapFinIdx f = [] ↔ l = []
-- Mathlib.Topology.UniformSpace.Equicontinuity
Filter.HasBasis.uniformEquicontinuousOn_iff_left : ∀ {ι : Type u_1} {κ : Type u_2} {α : Type u_6} {β : Type u_8} [uα : UniformSpace α] [uβ : UniformSpace β] {p : κ → Prop}
  {s : κ → Set (β × β)} {F : ι → β → α} {S : Set β},
  (uniformity β ⊓ Filter.principal (S ×ˢ S)).HasBasis p s →
    (UniformEquicontinuousOn F S ↔
      ∀ U ∈ uniformity α, ∃ k, p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (i : ι), (F i x, F i y) ∈ U)
-- Mathlib.CategoryTheory.Core
CategoryTheory.coreFunctor_map_app_iso_inv : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X Y : CategoryTheory.Core (CategoryTheory.Functor C D)} (η : X ⟶ Y) (X_1 : CategoryTheory.Core C),
  (((CategoryTheory.coreFunctor C D).map η).app X_1).iso.inv = η.iso.inv.app X_1.of
-- Mathlib.GroupTheory.PGroup
IsPGroup.comap_of_injective : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] {H : Subgroup G},
  IsPGroup p ↥H →
    ∀ {K : Type u_2} [inst_1 : Group K] (ϕ : K →* G), Function.Injective ⇑ϕ → IsPGroup p ↥(Subgroup.comap ϕ H)
-- Mathlib.RingTheory.FinitePresentation
AlgHom.FinitePresentation.comp_surjective : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : CommRing B] [inst_3 : CommRing C] [inst_4 : Algebra R A] [inst_5 : Algebra R B] [inst_6 : Algebra R C]
  {f : A →ₐ[R] B} {g : B →ₐ[R] C},
  f.FinitePresentation → Function.Surjective ⇑g → (RingHom.ker g.toRingHom).FG → (g.comp f).FinitePresentation
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- Given a measure upstairs (i.e., on `α`), and a choice `s` of fundamental domain, there's always
an artificial way to generate a measure downstairs such that the pair satisfies the
`QuotientMeasureEqMeasurePreimage` typeclass.  -/
MeasureTheory.IsFundamentalDomain.quotientMeasureEqMeasurePreimage_quotientMeasure : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α]
  {ν : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α ν] [Countable G] [MeasurableConstSMul G α]
  {s : Set α},
  MeasureTheory.IsFundamentalDomain G s ν →
    MeasureTheory.QuotientMeasureEqMeasurePreimage ν
      (MeasureTheory.Measure.map (Quotient.mk (MulAction.orbitRel G α)) (ν.restrict s))
-- Mathlib.Logic.Equiv.Defs
Equiv.equiv_subsingleton_dom : ∀ {α : Sort u} {β : Sort v} [Subsingleton α], Subsingleton (α ≃ β)
-- Mathlib.Analysis.Real.Hyperreal
/-- A sample infinitesimal hyperreal ε = ⟦(0, 1, 1/2, 1/3, ⋯)⟧. 

Conventions for notations in identifiers:

 * The recommended spelling of `ε` in identifiers is `epsilon`. -/
Hyperreal.epsilon : ℝ*
-- Std.Tactic.BVDecide.Normalize.Equal
Std.Tactic.BVDecide.Frontend.Normalize.BitVec.allOnes_eq_and : ∀ {w : ℕ} (a b : BitVec w), (-1#w == a &&& b) = (a == -1#w && b == -1#w)
-- Mathlib.Algebra.Order.BigOperators.Expect
/-- Positivity extension for `Finset.expect`.  -/
Mathlib.Meta.Positivity.evalFinsetExpect : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Order.RelIso.Basic
RelEmbedding.sumLiftRelInr_apply : ∀ {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) (val : β),
  (RelEmbedding.sumLiftRelInr r s) val = Sum.inr val
-- Mathlib.Topology.MetricSpace.Infsep
Set.einfsep_pair_le_left : ∀ {α : Type u_1} [inst : EDist α] {x y : α}, x ≠ y → {x, y}.einfsep ≤ edist x y
-- Mathlib.RingTheory.FiniteLength
IsFiniteLength.of_subsingleton : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Subsingleton M],
  IsFiniteLength R M
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey_union_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  (mem : k ∈ t₂), (t₁ ∪ t₂).getKey k ⋯ = t₂.getKey k mem
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.IsStableUnderCoproductsOfShape.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (J : Type u_1)
  [W.RespectsIso],
  (∀ (X₁ X₂ : J → C) [inst_2 : CategoryTheory.Limits.HasCoproduct X₁] [inst_3 : CategoryTheory.Limits.HasCoproduct X₂]
      (f : (j : J) → X₁ j ⟶ X₂ j), (∀ (j : J), W (f j)) → W (CategoryTheory.Limits.Sigma.map f)) →
    W.IsStableUnderCoproductsOfShape J
-- Batteries.Data.Fin.Coding
Fin.encodePUnit_decodePUnit : ∀ (x : Fin 1), Fin.encodePUnit (Fin.decodePUnit x) = x
-- Plausible.DeriveArbitrary
/-- Variant of `Deriving.Util.mkHeader` where we don't add an explicit binder
of the form `($targetName : $targetType)` to the field `binders`
(i.e. `binders` contains only implicit binders)  -/
_private.Plausible.DeriveArbitrary.0.Plausible.mkHeaderWithOnlyImplicitBinders : Lean.Name → ℕ → Lean.InductiveVal → Lean.Elab.TermElabM Lean.Elab.Deriving.Header
-- Mathlib.Tactic.Translate.Reorder
/-- Return the permutation that sends `src` to `tgt`, if it exists.  -/
Mathlib.Tactic.Translate.getPermutation : {α : Type u_1} → [BEq α] → Array α → Array α → Option Mathlib.Tactic.Translate.Permutation
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Hom.mk : {L : FirstOrder.Language} →
  {M : Type w} →
    {N : Type w'} →
      [inst : L.Structure M] →
        [inst_1 : L.Structure N] →
          (toFun : M → N) →
            autoParam
                (∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M),
                  toFun (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (toFun ∘ x))
                FirstOrder.Language.Hom.map_fun'._autoParam →
              autoParam
                  (∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M),
                    FirstOrder.Language.Structure.RelMap r x → FirstOrder.Language.Structure.RelMap r (toFun ∘ x))
                  FirstOrder.Language.Hom.map_rel'._autoParam →
                L.Hom M N
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.ofList_nil : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}, Std.ExtDTreeMap.ofList [] cmp = ∅
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.dfoldCast_trans : ∀ {i n j k : ℕ} {α : (i : ℕ) → autoParam (i ≤ n) Nat.dfoldCast._auto_1✝ → Type u_1} (h : i ≤ n) (w₁ : i = j)
  (w₂ : j = k) (x : α i h), Nat.dfoldCast✝ α w₂ (Nat.dfoldCast✝ α w₁ x) = Nat.dfoldCast✝ α ⋯ x
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.add_pf_add_zero : ∀ {R : Type u_1} [inst : CommSemiring R] (a : R), a + 0 = a
-- Lean.Server.FileWorker.SemanticHighlighting
/-- In case of overlap, higher-priority tokens will take precedence  -/
Lean.Server.FileWorker.LeanSemanticToken.priority : Lean.Server.FileWorker.LeanSemanticToken → ℕ
-- Batteries.Data.List.Basic
List.sigma_eq_sigmaTR : @List.sigma = @List.sigmaTR
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.Hover : Type
-- Init.Data.Slice.List.Lemmas
List.toList_mkSlice_roo : ∀ {α : Type u_1} {xs : List α} {lo hi : ℕ},
  Std.Slice.toList (Std.Roo.Sliceable.mkSlice xs lo<...hi) = List.drop (lo + 1) (List.take hi xs)
-- Mathlib.Analysis.CStarAlgebra.Multiplier
/-- The star operation on `a : 𝓜(𝕜, A)` is given by
`(star a).toProd = (star ∘ a.snd ∘ star, star ∘ a.fst ∘ star)`.  -/
DoubleCentralizer.instStar : {𝕜 : Type u_1} →
  {A : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NonUnitalNormedRing A] →
        [inst_2 : NormedSpace 𝕜 A] →
          [inst_3 : SMulCommClass 𝕜 A A] →
            [inst_4 : IsScalarTower 𝕜 A A] →
              [inst_5 : StarRing 𝕜] →
                [inst_6 : StarRing A] → [StarModule 𝕜 A] → [NormedStarGroup A] → Star (DoubleCentralizer 𝕜 A)
-- Mathlib.Algebra.Homology.HomologySequence
HomologicalComplex.homologyFunctor.congr_simp : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} (c : ComplexShape ι) (i i_1 : ι),
  i = i_1 →
    ∀ [inst_2 : CategoryTheory.CategoryWithHomology C],
      HomologicalComplex.homologyFunctor C c i = HomologicalComplex.homologyFunctor C c i_1
-- Mathlib.Analysis.Normed.Group.HomCompletion
normedAddGroupHomCompletionHom_apply : ∀ {G : Type u_1} [inst : SeminormedAddCommGroup G] {H : Type u_2} [inst_1 : SeminormedAddCommGroup H]
  (f : NormedAddGroupHom G H), normedAddGroupHomCompletionHom f = f.completion
-- Mathlib.RingTheory.HahnSeries.Multiplication
/-- We introduce a type alias for `HahnSeries` in order to work with scalar multiplication by
series. If we wrote a `SMul R⟦Γ⟧ V⟦Γ⟧` instance, then when
`V = R⟦Γ⟧`, we would have two different actions of `R⟦Γ⟧` on `V⟦Γ⟧`.
See `Mathlib/Algebra/Polynomial/Module/Basic.lean` for more discussion on this problem.  -/
HahnModule : (Γ : Type u_6) → (R : Type u_7) → (V : Type u_8) → [PartialOrder Γ] → [Zero V] → [SMul R V] → Type (max u_6 u_8)
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.Indep.insert_indep_iff : ∀ {α : Type u_2} {M : Matroid α} {e : α} {I : Set α}, M.Indep I → (M.Indep (insert e I) ↔ e ∈ M.E \ M.closure I ∨ e ∈ I)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.uset.congr_simp : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId fvarId_1 : Lean.FVarId),
  fvarId = fvarId_1 →
    ∀ (i i_1 : ℕ),
      i = i_1 →
        ∀ (y y_1 : Lean.FVarId),
          y = y_1 →
            ∀ (k k_1 : Lean.Compiler.LCNF.Code pu),
              k = k_1 →
                ∀ (h : pu = Lean.Compiler.LCNF.Purity.impure),
                  Lean.Compiler.LCNF.Code.uset fvarId i y k h = Lean.Compiler.LCNF.Code.uset fvarId_1 i_1 y_1 k_1 h
-- Mathlib.Data.TwoPointing
TwoPointing.mk.inj : ∀ {α : Type u_3} {toProd : α × α} {fst_ne_snd : toProd.1 ≠ toProd.2} {toProd_1 : α × α}
  {fst_ne_snd_1 : toProd_1.1 ≠ toProd_1.2},
  { toProd := toProd, fst_ne_snd := fst_ne_snd } = { toProd := toProd_1, fst_ne_snd := fst_ne_snd_1 } →
    toProd = toProd_1
-- Init.Grind.Config
/-- If `splitIndPred` is `true`, `grind` performs case-splitting on inductive predicates.
Otherwise, it performs case-splitting only on types marked with `[grind cases]` attribute.  -/
Lean.Grind.Config.splitIndPred : Lean.Grind.Config → Bool
-- Mathlib.Analysis.InnerProductSpace.Positive
ContinuousLinearMap.isPositive_one : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E],
  ContinuousLinearMap.IsPositive 1
-- Mathlib.Data.Finsupp.Fin
Finsupp.cons_ne_zero_iff : ∀ {n : ℕ} {M : Type u_1} [inst : Zero M] {y : M} {s : Fin n →₀ M}, Finsupp.cons y s ≠ 0 ↔ y ≠ 0 ∨ s ≠ 0
-- Lean.Elab.Do.Legacy
/-- Auxiliary operation for adding new variables to the collection of updated variables in a CodeBlock.
When a new variable is not already in the collection, but is shadowed by some declaration in `c`,
we create auxiliary join points to make sure we preserve the semantics of the code block.
Example: suppose we have the code block `print x; let x := 10; return x`. And we want to extend it
with the reassignment `x := x + 1`. We first use `pullExitPoints` to create
```
let jp (x!1) :=  return x!1;
print x;
let x := 10;
jmp jp x
```
and then we add the reassignment
```
x := x + 1
let jp (x!1) := return x!1;
print x;
let x := 10;
jmp jp x
```
Note that we created a fresh variable `x!1` to avoid accidental name capture.
As another example, consider
```
print x;
let x := 10
y := y + 1;
return x;
```
We transform it into
```
let jp (y x!1) := return x!1;
print x;
let x := 10
y := y + 1;
jmp jp y x
```
and then we add the reassignment as in the previous example.
We need to include `y` in the jump, because each exit point is implicitly returning the set of
update variables.

We implement the method as follows. Let `us` be `c.uvars`, then
1- for each `return _ y` in `c`, we create a join point
  `let j (us y!1) := return y!1`
   and replace the `return _ y` with `jmp us y`
2- for each `break`, we create a join point
  `let j (us) := break`
   and replace the `break` with `jmp us`.
3- Same as 2 for `continue`.
 -/
Lean.Elab.Term.Do.pullExitPoints : Lean.Elab.Term.Do.Code → Lean.Elab.TermElabM Lean.Elab.Term.Do.Code
-- Mathlib.RingTheory.PicardGroup
Module.Invertible.of_isLocalization : ∀ {R : Type u} {M : Type v} {N : Type u_1} {A : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] [Module.Invertible R M]
  [inst_6 : CommSemiring A] [inst_7 : Algebra R A] (S : Submonoid R) [IsLocalization S A] (f : M →ₗ[R] N)
  [IsLocalizedModule S f] [inst_10 : Module A N] [IsScalarTower R A N], Module.Invertible A N
-- Mathlib.CategoryTheory.Limits.Final
/-- A functor `F : C ⥤ D` is final if for every `d : D`, the comma category of morphisms `d ⟶ F.obj c`
is connected.  -/
CategoryTheory.Functor.Final : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → Prop
-- Init.Grind.Lemmas
Lean.Grind.imp_eq_of_eq_true_right : ∀ {a b : Prop}, b = True → (a → b) = True
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get_congr : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a b : α} (hab : (a == b) = true) {h' : a ∈ m},
  Std.ExtDHashMap.Const.get m a h' = Std.ExtDHashMap.Const.get m b ⋯
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasurableEquiv.sigmaFinite_map : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  (f : α ≃ᵐ β) [MeasureTheory.SigmaFinite μ], MeasureTheory.SigmaFinite (MeasureTheory.Measure.map (⇑f) μ)
-- Mathlib.Order.UpperLower.Principal
LowerSet.map_Iic : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β) (a : α),
  (LowerSet.map f) (LowerSet.Iic a) = LowerSet.Iic (f a)
-- Mathlib.CategoryTheory.Limits.Types.Pullbacks
/-- The usual explicit pullback in the category of types, as a subtype of the product.
The full `LimitCone` data is bundled as `pullbackLimitCone f g`.
 -/
CategoryTheory.Limits.Types.PullbackObj : {X Y Z : Type u} → (X ⟶ Z) → (Y ⟶ Z) → Type u
-- Mathlib.Algebra.Order.Monoid.Units
Units.orderEmbeddingVal_apply : ∀ {α : Type u_1} [inst : Monoid α] [inst_1 : LinearOrder α], ⇑Units.orderEmbeddingVal = Units.val