mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.hom_inv_actionHomLeft : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {x y : C} (f : x ≅ y) (z : D),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f.hom z)
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f.inv z) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj x z)
-- Mathlib.Algebra.Notation.Defs
/-- Notation typeclass (with no default notation!) for an algebraic structure with a star operation.
 -/
Star : Type u → Type u
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- Given `f : L →ₐ[K] L'`, `S.map f` is the intermediate field between `K` and `L'`
such that `x ∈ S ↔ f x ∈ S.map f`.  -/
IntermediateField.map : {K : Type u_1} →
  {L : Type u_2} →
    {L' : Type u_3} →
      [inst : Field K] →
        [inst_1 : Field L] →
          [inst_2 : Field L'] →
            [inst_3 : Algebra K L] →
              [inst_4 : Algebra K L'] → (L →ₐ[K] L') → IntermediateField K L → IntermediateField K L'
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RioSlice : (α : Type u_1) → Type u_2 → [Ord α] → Type (max u_2 u_1)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.Pos.skip?_eq_none_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s : String.Slice} {pos : s.Pos}, pos.skip? pat = none ↔ ¬String.Slice.Pattern.Model.MatchesAt pat pos
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.mapShortComplexH2.eq_1 : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B),
  groupHomology.mapShortComplexH2 f φ =
    { τ₁ := groupHomology.chainsMap₃ f φ, τ₂ := groupHomology.chainsMap₂ f φ, τ₃ := groupHomology.chainsMap₁ f φ,
      comm₁₂ := ⋯, comm₂₃ := ⋯ }
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.instInhabitedAtomIso : Inhabited Mathlib.Tactic.BicategoryLike.AtomIso
-- Mathlib.Probability.Kernel.Disintegration.CondCDF
MeasureTheory.Measure.IicSnd_le_fst : ∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (r : ℝ), ρ.IicSnd r ≤ ρ.fst
-- Mathlib.Tactic.TermCongr
/-- Get the sides of the type of `pf` and unify them with the respective `lhs` and `rhs`.  -/
_private.Mathlib.Tactic.TermCongr.0.Mathlib.Tactic.TermCongr.CongrResult.mk'.ensureSidesDefeq : Lean.Expr → Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.insertIdxTR.go.eq_1 : ∀ {α : Type u_1} (a : α) (a_1 : List α) (a_2 : Array α), List.insertIdxTR.go✝ a 0 a_1 a_2 = a_2.toListAppend (a :: a_1)
-- Mathlib.Topology.MetricSpace.Similarity
/-- Similarity holds if and only if all distances are proportional.  -/
similar_iff_exists_dist_eq : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoMetricSpace P₁]
  [inst_1 : PseudoMetricSpace P₂],
  Similar v₁ v₂ ↔ ∃ r, r ≠ 0 ∧ ∀ (i₁ i₂ : ι), dist (v₁ i₁) (v₁ i₂) = ↑r * dist (v₂ i₁) (v₂ i₂)
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.false_and : ∀ {σs : List (Type u)} {P : Std.Do.SPred σs}, ⌜False⌝ ∧ P ⊣⊢ₛ ⌜False⌝
-- Mathlib.Topology.Order.Basic
OrderTopology.continuous_iff : ∀ {α : Type u} {β : Type v} [ts : TopologicalSpace α] [inst : Preorder α] [OrderTopology α]
  [inst_2 : TopologicalSpace β] {f : β → α},
  Continuous f ↔ ∀ (a : α), IsOpen (f ⁻¹' Set.Ioi a) ∧ IsOpen (f ⁻¹' Set.Iio a)
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
/-- **Alias** of `FunLike.coe_add`. -/
SlashInvariantForm.coe_add : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Add F] [inst_2 : Add β]
  [IsAddApply F α β] (f g : F), ⇑(f + g) = ⇑f + ⇑g
-- Mathlib.RepresentationTheory.Homological.Resolution
/-- The free functor `Type u ⥤ ModuleCat.{u} k` applied to the universal cover of the classifying
space of `G` as a simplicial set, augmented by the map from `Fin 1 → G` to the terminal object
in `Type u`.  -/
classifyingSpaceUniversalCover.compForgetAugmented.toModule : (k G : Type u) → [inst : CommRing k] → [Monoid G] → CategoryTheory.SimplicialObject.Augmented (ModuleCat k)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G)
  (x : ↑((CategoryTheory.forget₂ (Rep.{u, u, u} k G) (ModuleCat k)).obj A)),
  (CategoryTheory.ConcreteCategory.hom (groupHomology.opcyclesIso₀ A).inv) ((Representation.Coinvariants.mk A.ρ) x) =
    (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.pOpcycles (groupHomology.inhomogeneousChains A) 0))
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.chainsIso₀ A).inv) x)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.maxKey?.eq_3 : ∀ {α : Type u} {β : α → Type v} (size : ℕ) (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β) (size_1 : ℕ) (k_1 : α)
  (v_1 : β k_1) (l_1 r : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)).maxKey? =
    (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r).maxKey?
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearEquiv.isAdjointPair_symm_iff : ∀ {R : Type u_20} {M : Type u_21} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {B : LinearMap.BilinForm R M} {f : M ≃ M}, LinearMap.IsAdjointPair B B ⇑f ⇑f.symm ↔ LinearMap.IsOrthogonal B ⇑f
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.SimpleFunc.setToSimpleFunc_zero' : ∀ {α : Type u_1} {E : Type u_2} {F' : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F'] [inst_3 : NormedSpace ℝ F'] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F'},
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = 0) →
    ∀ (f : MeasureTheory.SimpleFunc α E),
      MeasureTheory.Integrable (⇑f) μ → MeasureTheory.SimpleFunc.setToSimpleFunc T f = 0
-- Init.System.IO
/-- An `IO` monad that cannot throw exceptions.
 -/
BaseIO : Type → Type
-- Mathlib.Data.Holor
HolorIndex.assocRight.eq_1 : ∀ {ds₁ ds₂ ds₃ : List ℕ}, HolorIndex.assocRight = cast ⋯
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- Auxiliary lemma in the proof of `integral_eq_sub_of_hasDeriv_right_of_le`: real version  -/
intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le_real : ∀ {g' g : ℝ → ℝ} {a b : ℝ},
  a ≤ b →
    ContinuousOn g (Set.Icc a b) →
      (∀ x ∈ Set.Ioo a b, HasDerivWithinAt g (g' x) (Set.Ioi x) x) →
        MeasureTheory.IntegrableOn g' (Set.Icc a b) MeasureTheory.volume → ∫ (y : ℝ) in a..b, g' y = g b - g a
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.Poly.coeff.match_1.splitter : (motive : Int.Internal.Linear.Poly → Sort u_1) →
  (p : Int.Internal.Linear.Poly) →
    ((a : ℤ) →
        (y : Int.Internal.Linear.Var) → (p : Int.Internal.Linear.Poly) → motive (Int.Internal.Linear.Poly.add a y p)) →
      ((k : ℤ) → motive (Int.Internal.Linear.Poly.num k)) → motive p
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.exists_lift_of_mem_range_rTensor : ∀ {R : Type u} [inst : CommSemiring R] {M : Type u_1} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Type v}
  [inst_3 : CommSemiring S] [inst_4 : Algebra R S] {T : Type u_3} [inst_5 : CommSemiring T] [inst_6 : Algebra R T]
  (A : Subalgebra R T) {φ : S →ₐ[R] T},
  A ≤ φ.range →
    ∀ {t : TensorProduct R T M},
      t ∈ (LinearMap.rTensor M A.val.toLinearMap).range → ∃ s, (LinearMap.rTensor M φ.toLinearMap) s = t
-- Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
/-- The `vonMangoldt` function is the function on natural numbers that returns `log p` if the input can
be expressed as `p^k` for a prime `p`.
In the case when `n` is a prime power, `Nat.minFac` will give the appropriate prime, as it is the
smallest prime factor.

In the `ArithmeticFunction` locale, we have the notation `Λ` for this function.
This is also available in the `ArithmeticFunction.vonMangoldt` locale, allowing for selective
access to the notation.
 -/
ArithmeticFunction.termΛ : Lean.ParserDescr
-- Mathlib.Tactic.Algebra.Lemmas
Mathlib.Tactic.Algebra.isRat_eq_rawCast : ∀ {R : Type u_1} {A : Type u_2} [inst : Field R] [inst_1 : Field A] [inst_2 : Algebra R A] {a : A} {n d : ℕ},
  Mathlib.Meta.NormNum.IsRat a (Int.negOfNat n) d → a = (algebraMap R A) (Rat.rawCast (Int.negOfNat n) d + 0) + 0
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.toArray_filter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {f : α → β → Bool},
  (Std.TreeMap.filter f t).toArray = Array.filter (fun p => f p.1 p.2) t.toArray
-- Mathlib.Topology.GDelta.Basic
countableInterFilter_residual : ∀ {X : Type u_1} [inst : TopologicalSpace X], CountableInterFilter (residual X)
-- Mathlib.Topology.EMetricSpace.Lipschitz
continuousOn_prod_of_continuousOn_lipschitzOnWith' : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : TopologicalSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : PseudoEMetricSpace γ] (f : α × β → γ) {s : Set α} {t : Set β} (K : NNReal),
  (∀ a ∈ s, LipschitzOnWith K (fun y => f (a, y)) t) →
    (∀ b ∈ t, ContinuousOn (fun x => f (x, b)) s) → ContinuousOn f (s ×ˢ t)
-- Init.Tactics
/-- `apply_rules [l₁, l₂, ...]` tries to solve the main goal by iteratively
applying the list of lemmas `[l₁, l₂, ...]` or by applying a local hypothesis.
If `apply` generates new goals, `apply_rules` iteratively tries to solve those goals.
You can use `apply_rules [-h]` to omit a local hypothesis.

`apply_rules` will also use `rfl`, `trivial`, `congrFun` and `congrArg`.
These can be disabled, as can local hypotheses, by using `apply_rules only [...]`.

You can use `apply_rules using [a₁, ...]` to use all lemmas which have been labelled
with the attributes `aᵢ` (these attributes must be created using `register_label_attr`).

You can pass a further configuration via the syntax `apply_rules (config := {...})`.
The options supported are the same as for `solve_by_elim` (and include all the options for `apply`).

`apply_rules` will try calling `symm` on hypotheses and `exfalso` on the goal as needed.
This can be disabled with `apply_rules (config := {symm := false, exfalso := false})`.

You can bound the iteration depth using the syntax `apply_rules (config := {maxDepth := n})`.

Unlike `solve_by_elim`, `apply_rules` does not perform backtracking, and greedily applies
a lemma from the list until it gets stuck.
 -/
Lean.Parser.Tactic.applyRules : Lean.ParserDescr
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.inv_invApp : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f]
  (U : TopologicalSpace.Opens ↑X.toTopCat),
  CategoryTheory.inv (AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp f U) =
    CategoryTheory.CategoryStruct.comp
      (f.c.app (Opposite.op ((AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.opensFunctor f).obj U)))
      (X.presheaf.map (CategoryTheory.eqToHom ⋯))
-- Mathlib.Data.Set.Prod
/-- The diagonal $\Delta(X) \subseteq X \times_Y X$.  -/
Function.pullbackDiagonal : {X : Type u_1} → {Y : Sort u_2} → (f : X → Y) → Set (Function.Pullback f f)
-- Mathlib.Data.ENNReal.Operations
ENNReal.le_iInf₂_add_iInf₂ : ∀ {ι : Sort u_1} {a : ENNReal} {κ : Sort u_2} {q₁ : ι → Sort u_3} {q₂ : κ → Sort u_4} {f : (i : ι) → q₁ i → ENNReal}
  {g : (k : κ) → q₂ k → ENNReal},
  (∀ (i : ι) (pi : q₁ i) (k : κ) (qk : q₂ k), a ≤ f i pi + g k qk) → a ≤ (⨅ i, ⨅ qi, f i qi) + ⨅ k, ⨅ qk, g k qk
-- Mathlib.Algebra.Order.Group.Indicator
Set.mulIndicator_le_mulIndicator_apply_of_subset : ∀ {α : Type u_2} {M : Type u_3} [inst : Preorder M] [inst_1 : One M] {s t : Set α} {f : α → M} {a : α},
  s ⊆ t → 1 ≤ f a → s.mulIndicator f a ≤ t.mulIndicator f a
-- Mathlib.Analysis.Convex.Intrinsic
ContinuousAffineEquiv.intrinsicFrontier_image : ∀ {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} {Q : Type u_4} {P : Type u_5} [inst : Ring 𝕜] [inst_1 : AddCommGroup V]
  [inst_2 : AddCommGroup W] [inst_3 : Module 𝕜 V] [inst_4 : Module 𝕜 W] [inst_5 : TopologicalSpace P]
  [inst_6 : TopologicalSpace Q] [inst_7 : AddTorsor V P] [inst_8 : AddTorsor W Q] (φ : P ≃ᴬ[𝕜] Q) (s : Set P),
  intrinsicFrontier 𝕜 (⇑φ '' s) = ⇑φ '' intrinsicFrontier 𝕜 s
-- Mathlib.Data.Stream.Init
Stream'.iterate_eq : ∀ {α : Type u} (f : α → α) (a : α), Stream'.iterate f a = Stream'.cons a (Stream'.iterate f (f a))
-- Mathlib.CategoryTheory.Localization.Predicate
/-- The functor `(D ⥤ E) ⥤ W.functors_inverting E` induced by the composition
with a localization functor `L : C ⥤ D` with respect to `W : MorphismProperty C`.  -/
CategoryTheory.Localization.whiskeringLeftFunctor : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (L : CategoryTheory.Functor C D) →
          (W : CategoryTheory.MorphismProperty C) →
            (E : Type u_3) →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} E] →
                [L.IsLocalization W] → CategoryTheory.Functor (CategoryTheory.Functor D E) (W.FunctorsInverting E)
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isLittleO_iff_exists_eq_mul : ∀ {α : Type u_1} {𝕜 : Type u_15} [inst : NormedDivisionRing 𝕜] {l : Filter α} {u v : α → 𝕜},
  u =o[l] v ↔ ∃ φ, Filter.Tendsto φ l (nhds 0) ∧ u =ᶠ[l] φ * v
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.PartialEquiv.symm_apply : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f : L.PartialEquiv M N) (x : ↥f.cod), f.symm.toEquiv x = f.toEquiv.symm x
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.uniqueHomToTrivial : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      (A : CategoryTheory.AddGrp C) → Unique (A ⟶ CategoryTheory.AddGrp.trivial C)
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.below.zero_add : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  {motive : (a a_1 : RingCat.Colimits.Prequotient F) → RingCat.Colimits.Relation F a a_1 → Prop}
  (x : RingCat.Colimits.Prequotient F), RingCat.Colimits.Relation.below ⋯
-- Aesop.Forward.Substitution
/-- Open the type of a rule `e`. If a substitution `σ` is given, this function
acts like `Substitution.openRuleType σ`. Otherwise it acts like
`forallMetaTelescope`.  -/
Aesop.openRuleType : Option Aesop.Substitution → Lean.Expr → Lean.MetaM (Array Lean.MVarId × Array Lean.BinderInfo × Lean.Expr)
-- Lean.DocString.Extension
Lean.VersoModuleDocs.instReprSnippet.repr : Lean.VersoModuleDocs.Snippet → ℕ → Std.Format
-- Mathlib.CategoryTheory.PathCategory.Basic
CategoryTheory.Paths.lift_spec : ∀ {V : Type u₁} [inst : Quiver V] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C] (φ : V ⥤q C),
  CategoryTheory.Paths.of V ⋙q (CategoryTheory.Paths.lift φ).toPrefunctor = φ
-- Lean.Elab.Tactic.Basic
_private.Lean.Elab.Tactic.Basic.0.Lean.Elab.Tactic.getMainGoal.loop : List Lean.MVarId → Lean.Elab.Tactic.TacticM Lean.MVarId
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
TwoSidedIdeal.asIdeal.eq_1 : ∀ {R : Type u_1} [inst : Ring R],
  TwoSidedIdeal.asIdeal =
    { toFun := fun I => { carrier := ↑I, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }, monotone' := ⋯ }
-- Mathlib.RingTheory.Bialgebra.Quotient
/-- The comultiplication on `A ⧸ I`, as an `R`-algebra homomorphism.  -/
Bialgebra.Quotient.comulAlgHom : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : Ring A] →
        [inst_2 : Bialgebra R A] →
          (I : Ideal A) →
            [inst_3 : I.IsTwoSided] →
              [(Submodule.restrictScalars R I).IsCoideal] → A ⧸ I →ₐ[R] TensorProduct R (A ⧸ I) (A ⧸ I)
-- Mathlib.CategoryTheory.Sums.Products
CategoryTheory.Sum.natIsoOfWhiskerLeftInlInr_eq : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {A' : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] {B : Type u} [inst_2 : CategoryTheory.Category.{v, u} B]
  {F G : CategoryTheory.Functor (A ⊕ A') B}
  (η₁ : (CategoryTheory.Sum.inl_ A A').comp F ≅ (CategoryTheory.Sum.inl_ A A').comp G)
  (η₂ : (CategoryTheory.Sum.inr_ A A').comp F ≅ (CategoryTheory.Sum.inr_ A A').comp G),
  CategoryTheory.Sum.natIsoOfWhiskerLeftInlInr η₁ η₂ =
    (CategoryTheory.Sum.functorEquiv A A' B).unitIso.app F ≪≫
      (CategoryTheory.Sum.functorEquiv A A' B).inverse.mapIso (η₁.prod η₂) ≪≫
        (CategoryTheory.Sum.functorEquiv A A' B).unitIso.symm.app G
-- 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 α] (h : t.WF)
  {k : α} {v : β},
  (Std.DTreeMap.Internal.Impl.Const.getThenInsertIfNew? t k v ⋯).1 = Std.DTreeMap.Internal.Impl.Const.get? t k
-- Std.Data.HashMap.IteratorLemmas
Std.HashMap.toListRev_valuesIter : ∀ {α β : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap α β},
  m.valuesIter.toListRev = (List.map Prod.snd m.toList).reverse
-- Mathlib.Algebra.Prime.Defs
Prime.not_isUnit : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {p : M}, Prime p → ¬IsUnit p
-- Init.Ext
Sigma.ext : ∀ {α : Type u} {β : α → Type v} {x y : Sigma β}, x.fst = y.fst → x.snd ≍ y.snd → x = y
-- Mathlib.Topology.Order.Monotone
IsClosed.sSup_mem : ∀ {α : Type u_1} [inst : CompleteLinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α] {s : Set α},
  s.Nonempty → IsClosed s → sSup s ∈ s
-- Mathlib.SetTheory.Lists
Lists'.Subset.cons : ∀ {α : Type u_1} {a a' : Lists α} {l l' : Lists' α true},
  a.Equiv a' → a' ∈ l'.toList → l.Subset l' → (Lists'.cons a l).Subset l'
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.iSup.congr_simp : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} {n : ℕ} [inst : Finite β] (f f_1 : β → L.BoundedFormula α n),
  f = f_1 → FirstOrder.Language.BoundedFormula.iSup f = FirstOrder.Language.BoundedFormula.iSup f_1
-- Mathlib.Geometry.Euclidean.Volume.Measure
_private.Mathlib.Geometry.Euclidean.Volume.Measure.0.Submodule.measurableEquivProd.eq_1 : ∀ {V : Type u_3} {P : Type u_4} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
  [inst_2 : MeasurableSpace V] [inst_3 : BorelSpace V] [inst_4 : FiniteDimensional ℝ V] [inst_5 : MetricSpace P]
  [inst_6 : MeasurableSpace P] [inst_7 : BorelSpace P] [inst_8 : NormedAddTorsor V P] (s : Submodule ℝ V) (p : P),
  s.measurableEquivProd p =
    (IsometryEquiv.vaddConst p).toHomeomorph.toMeasurableEquiv.symm.trans
      (s.orthogonalDecomposition.toHomeomorph.toMeasurableEquiv.trans (MeasurableEquiv.toLp 2 (↥s × ↥sᗮ)).symm)
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.symm_h₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂),
  h.symm.h₁ = -h.h₁
-- Mathlib.Data.FinEnum.Option
/-- For a type with positive `card`, the recursion principle evaluates to whatever
`congr` makes of the step result, where `Option.none` has been inserted into the
`(finChoice (card α - 1))`th rank of the enumeration.
 -/
FinEnum.recEmptyOption_of_card_pos : ∀ {P : Type u → Sort v} (finChoice : (n : ℕ) → Fin (n + 1))
  (congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → FinEnum.card β = FinEnum.card α → P α → P β)
  (empty : P PEmpty.{u + 1}) (option : {α : Type u} → FinEnum α → P α → P (Option α)) (α : Type u) [inst : FinEnum α]
  (h : 0 < FinEnum.card α),
  FinEnum.recEmptyOption finChoice (fun {α β} => congr) empty (fun {α} => option) α =
    congr (FinEnum.insertNone (ULift.{u, 0} (Fin (FinEnum.card α - 1))) ↑↑(finChoice (FinEnum.card α - 1))) inst ⋯
      (option ULift.instFinEnum
        (FinEnum.recEmptyOption finChoice (fun {α β} => congr) empty (fun {α} => option)
          (ULift.{u, 0} (Fin (FinEnum.card α - 1)))))
-- Lean.Server.InfoUtils
Lean.Elab.Info.occursInside? : Lean.Elab.Info → String.Pos.Raw → Option String.Pos.Raw
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.proj_surjOn_baseSet : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  (e : Bundle.Pretrivialization F proj) [Nonempty F], Set.SurjOn proj e.source e.baseSet
-- Init.WF
Prod.instWellFoundedRelation : {α : Type u} → {β : Type v} → [ha : WellFoundedRelation α] → [hb : WellFoundedRelation β] → WellFoundedRelation (α × β)
-- Init.Data.SInt.Basic
instInhabitedISize : Inhabited ISize
-- Mathlib.Order.Cover
Prod.fst_eq_or_snd_eq_of_wcovBy : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : PartialOrder β] {x y : α × β},
  x ⩿ y → x.1 = y.1 ∨ x.2 = y.2
-- Mathlib.RingTheory.RingInvo
RingInvoClass.mk : ∀ {F : Type u_3} {R : Type u_4} [inst : Semiring R] [inst_1 : EquivLike F R Rᵐᵒᵖ]
  [toRingEquivClass : RingEquivClass F R Rᵐᵒᵖ],
  (∀ (f : F) (x : R), MulOpposite.unop (f (MulOpposite.unop (f x))) = x) → RingInvoClass F R
-- Mathlib.Topology.UniformSpace.Closeds
hausdorffEntourage.eq_1 : ∀ {α : Type u_1} (U : SetRel α α), hausdorffEntourage U = {x | x.1 ⊆ U.preimage x.2 ∧ x.2 ⊆ U.image x.1}
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
/-- The isomorphism `(K.extend e).homology j' ≅ K.homology j` when `e.f j = j'`.  -/
HomologicalComplex.extendHomologyIso : {ι : 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] →
              [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
                (K : HomologicalComplex C c) →
                  (e : c.Embedding c') →
                    {j : ι} →
                      {j' : ι'} →
                        e.f j = j' →
                          [inst_3 : K.HasHomology j] →
                            [inst_4 : (K.extend e).HasHomology j'] → (K.extend e).homology j' ≅ K.homology j
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rcc.eq_succMany?_of_toArray_eq_append_append : ∀ {α : Type u} {r : Std.Rcc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.Rxc.IsAlwaysFinite α] {pref suff : Array α} {cur : α} (h : r.toArray = pref ++ #[cur] ++ suff),
  cur = (Std.PRange.succMany? pref.size r.lower).get ⋯
-- Mathlib.Algebra.Order.Floor.Ring
/-- Extension for the `positivity` tactic: `Int.ceil` is positive/nonnegative if its input is.  -/
Mathlib.Meta.Positivity.evalIntCeil : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Data.Int.ModEq
Int.ModEq.add_right_cancel : ∀ {n a b c d : ℤ}, c ≡ d [ZMOD n] → a + c ≡ b + d [ZMOD n] → a ≡ b [ZMOD n]