mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.mapLeftHomologyIso_inv_naturality_assoc : ∀ {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.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : S₁.HasLeftHomology]
  [inst_6 : S₂.HasLeftHomology] [inst_7 : F.PreservesLeftHomologyOf S₁] [inst_8 : F.PreservesLeftHomologyOf S₂] {Z : D}
  (h : (S₂.map F).leftHomology ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.leftHomologyMap φ))
      (CategoryTheory.CategoryStruct.comp (S₂.mapLeftHomologyIso F).inv h) =
    CategoryTheory.CategoryStruct.comp (S₁.mapLeftHomologyIso F).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap (F.mapShortComplex.map φ)) h)
-- Mathlib.Algebra.Order.Sub.Defs
/-- See `lt_tsub_iff_right_of_le` for a weaker statement in a partial order.  -/
lt_tsub_iff_right : ∀ {α : Type u_1} {a b c : α} [inst : LinearOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α],
  a < b - c ↔ a + c < b
-- Mathlib.RingTheory.Extension.Generators
/-- A family of generators of an `R`-algebra `S` consists of
1. `ι`: The type of variables.
2. `val : ι → S`: The assignment of each variable to a value in `S`.
3. `σ`: A section of `R[X] → S`.  -/
Algebra.Generators : (R : Type u) →
  (S : Type v) → Type w → [inst : CommRing R] → [inst_1 : CommRing S] → [Algebra R S] → Type (max (max u v) w)
-- Mathlib.Analysis.LocallyConvex.HahnBanach
/-- **Hahn-Banach theorem** for linear functionals dominated by a continuous seminorm on
polynormable spaces over fields satisfying `IsRCLikeNormedField`.  -/
Module.Dual.exists_continuous_extension_of_le_seminorm : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : AddCommGroup E] [inst_1 : NormedField 𝕜] [IsRCLikeNormedField 𝕜]
  [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜 E] [PolynormableSpace 𝕜 E] (S : Submodule 𝕜 E) (f : Module.Dual 𝕜 ↥S)
  {p : Seminorm 𝕜 E},
  Continuous ⇑p → (∀ (x : ↥S), ‖f x‖ ≤ p ↑x) → ∃ g, (∀ (x : ↥S), g ↑x = f x) ∧ ∀ (x : E), ‖g x‖ ≤ p x
-- Mathlib.Analysis.Normed.Operator.Basic
ContinuousLinearMap.seminorm.congr_simp : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂],
  ContinuousLinearMap.seminorm = ContinuousLinearMap.seminorm
-- Lean.Linter.Sets
/-- Add a new linter set that contains the given linters.  -/
Lean.Linter.insertLinterSet : {m : Type → Type} → [Lean.MonadEnv m] → Lean.Name → Lean.NameSet → m Unit
-- Mathlib.InformationTheory.KullbackLeibler.Basic
/-- **Gibbs' inequality**: the Kullback-Leibler divergence is nonnegative.
Note that since `klDiv` takes value in `ℝ≥0∞` (defined when it is finite as `ENNReal.ofReal (...)`),
it is nonnegative by definition. This lemma proves that the argument of `ENNReal.ofReal`
is also nonnegative.  -/
InformationTheory.integral_llr_add_sub_measure_univ_nonneg : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν],
  μ.AbsolutelyContinuous ν →
    MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ →
      0 ≤ ∫ (x : α), MeasureTheory.llr μ ν x ∂μ + ν.real Set.univ - μ.real Set.univ
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
ContinuousLinearEquiv.comp_right_hasFDerivWithinAt_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : F → G} {s : Set F} {x : E}
  {f' : F →L[𝕜] G}, HasFDerivWithinAt (f ∘ ⇑iso) (f' ∘SL ↑iso) (⇑iso ⁻¹' s) x ↔ HasFDerivWithinAt f f' s (iso x)
-- Mathlib.Dynamics.SymbolicDynamics.Basic
SymbolicDynamics.FullShift.MulSubshift.ofForbidden.eq_1 : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : Inhabited A] {G : Type u_2} [inst_2 : Monoid G]
  [inst_3 : IsLeftCancelMul G] [inst_4 : DiscreteTopology A] (F : Set (SymbolicDynamics.FullShift.Pattern A G)),
  SymbolicDynamics.FullShift.MulSubshift.ofForbidden F =
    { carrier := SymbolicDynamics.FullShift.mulForbidden F, isClosed := ⋯, mapsTo := ⋯ }
-- Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
/-- If `K` is the field of fractions of the Dedekind domain `R` then `FiniteAdeleRing R K` is
the ring of finite adeles of `K`, defined as the restricted product of the completions
`K_v` with respect to the subrings `R_v`. Here `v` runs through the nonzero primes of `R`
and the restricted product is the subring of `∏_v K_v` consisting of elements which
are in `R_v` for all but finitely many `v`.
 -/
IsDedekindDomain.FiniteAdeleRing : (R : Type u_1) →
  [inst : CommRing R] →
    [IsDedekindDomain R] →
      (K : Type u_2) → [inst_2 : Field K] → [inst_3 : Algebra R K] → [IsFractionRing R K] → Type (max u_2 u_1)
-- Std.Time.Date.Basic
Std.Time.instHAddOffsetOffset_25 : HAdd Std.Time.Hour.Offset Std.Time.Millisecond.Offset Std.Time.Millisecond.Offset
-- Mathlib.Algebra.Homology.Embedding.HomEquiv
ComplexShape.Embedding.homRestrict.f.eq_1 : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {e : c.Embedding c'} {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'} {L : HomologicalComplex C c}
  [inst_3 : e.IsRelIff] (ψ : K ⟶ L.extend e) (i : ι),
  ComplexShape.Embedding.homRestrict.f ψ i = CategoryTheory.CategoryStruct.comp (ψ.f (e.f i)) (L.extendXIso e ⋯).hom
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey_insert_le_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, (cmp ((t.insert k v).minKey ⋯) k).isLE = true
-- Lean.Elab.Tactic.Try
/-- Version of `evalAndSuggest` that wraps tactic suggestions with `by` for term mode.  -/
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.evalAndSuggestWithBy : Lean.Syntax →
  Lean.TSyntax `tactic →
    ℕ → Lean.Try.Config → optParam Lean.MessageData Lean.MessageData.nil → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.direction_affineSpan_pair_le_iff_exists_smul : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {p₁ q₁ p₂ q₂ : P},
  line[k, p₁, q₁].direction ≤ line[k, p₂, q₂].direction ↔ ∃ z, z • (q₂ -ᵥ p₂) = q₁ -ᵥ p₁
-- Mathlib.Analysis.InnerProductSpace.Defs
/-- The inner product function.  -/
Inner.inner : (𝕜 : Type u_4) → {E : Type u_5} → [self : Inner 𝕜 E] → E → E → 𝕜
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.neg : Int.Internal.Linear.Expr → Int.Internal.Linear.Expr
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Pred
Std.Tactic.BVDecide.Return.mk.inj : ∀ {aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit} {result : aig.ExtendingEntrypoint}
  {cache : Std.Tactic.BVDecide.BVExpr.Cache (↑result).aig} {result_1 : aig.ExtendingEntrypoint}
  {cache_1 : Std.Tactic.BVDecide.BVExpr.Cache (↑result_1).aig},
  { result := result, cache := cache } = { result := result_1, cache := cache_1 } → result = result_1 ∧ cache ≍ cache_1
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LitValue.uint16.inj : ∀ {val val_1 : UInt16}, Lean.Compiler.LCNF.LitValue.uint16 val = Lean.Compiler.LCNF.LitValue.uint16 val_1 → val = val_1
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Expressions for structural isomorphisms. We do not impose the condition `isStructural` since
it is not needed to write the tactic.  -/
Mathlib.Tactic.BicategoryLike.Structural : Type
-- Mathlib.Algebra.Module.CharacterModule
CharacterModule.eq_zero_of_character_apply : ∀ {A : Type uA} [inst : AddCommGroup A] {a : A}, (∀ (c : CharacterModule A), c a = 0) → a = 0
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_union : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h₁ : m₁.WF)
  (h₂ : m₂.WF) {k fallback : α}, (m₁.union m₂ ⋯ ⋯).getKeyD k fallback = m₂.getKeyD k (m₁.getKeyD k fallback)
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.rightFunc_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (X : CategoryTheory.Comma (CategoryTheory.Functor.id C) (CategoryTheory.Functor.id C)),
  CategoryTheory.Arrow.rightFunc.obj X = X.right
-- Mathlib.Order.Filter.Pointwise
/-- The filter `f • g` is generated by `{s • t | s ∈ f, t ∈ g}` in scope `Pointwise`.  -/
Filter.instSMul : {α : Type u_2} → {β : Type u_3} → [SMul α β] → SMul (Filter α) (Filter β)
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instAddCancelMonoid.eq_1 : ∀ {α : Type u_1} [inst : AddCancelMonoid α],
  AddOpposite.instAddCancelMonoid =
    { toAddLeftCancelMonoid := AddOpposite.instAddLeftCancelMonoid, toIsRightCancelAdd := ⋯ }
-- Mathlib.FieldTheory.RatFunc.Luroth
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.algEquiv.eq_1 : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)} (h : E ≠ ⊥),
  RatFunc.Luroth.algEquiv h =
    (RatFunc.algEquivOfTranscendental (RatFunc.Luroth.generator E) ⋯).trans (IntermediateField.equivOfEq ⋯)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
/-- A periodic function is interval integrable over one full period if and only if it is interval
integrable over any other full period.

Special case of `Function.Periodic.intervalIntegrable`.
 -/
Function.Periodic.intervalIntegrable_iff : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℝ → E} {T t₁ t₂ : ℝ},
  Function.Periodic f T →
    (IntervalIntegrable f MeasureTheory.volume t₁ (t₁ + T) ↔ IntervalIntegrable f MeasureTheory.volume t₂ (t₂ + T))
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
SzemerediRegularity.le_stepBound : id ≤ SzemerediRegularity.stepBound
-- Mathlib.Algebra.GroupWithZero.Hom
MonoidWithZeroHom.coe_ofClass : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β]
  [inst_2 : FunLike F α β] [inst_3 : MonoidWithZeroHomClass F α β] (f : F), ⇑(MonoidWithZeroHom.ofClass f) = ⇑f
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Mathlib.Meta.Positivity.log_nz_of_isRat_neg : ∀ {e : ℝ} {d : ℕ} {n : ℤ},
  Mathlib.Meta.NormNum.IsRat e n d → decide (↑n / ↑d < 0) = true → decide (-1 < ↑n / ↑d) = true → Real.log e ≠ 0
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- Construct a uniform structure from a distance function and metric space axioms  -/
UniformSpace.ofDist : {α : Type u} →
  (dist : α → α → ℝ) →
    (∀ (x : α), dist x x = 0) →
      (∀ (x y : α), dist x y = dist y x) → (∀ (x y z : α), dist x z ≤ dist x y + dist y z) → UniformSpace α
-- Mathlib.Order.Hom.Lattice
/-- Copy of an `InfHom` with a new `toFun` equal to the old one. Useful to fix definitional
equalities.  -/
InfHom.copy : {α : Type u_2} →
  {β : Type u_3} → [inst : Min α] → [inst_1 : Min β] → (f : InfHom α β) → (f' : α → β) → f' = ⇑f → InfHom α β
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.SemiringExpr : Type
-- Mathlib.Probability.Process.HittingTime
/-- `hittingBtwn` is nonincreasing with respect to the set.  -/
MeasureTheory.hittingBtwn_anti : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder ι] (u : ι → Ω → β) (n m : ι),
  Antitone fun x => MeasureTheory.hittingBtwn u x n m
-- Mathlib.RingTheory.HahnSeries.HEval
/-- A summable family given by scalar multiples of powers of a positive order Hahn series.

The scalar multiples are given by the coefficients of a power series.  -/
HahnSeries.SummableFamily.powerSeriesFamily : {Γ : Type u_1} →
  {R : Type u_3} →
    {V : Type u_4} →
      [inst : AddCommMonoid Γ] →
        [inst_1 : LinearOrder Γ] →
          [IsOrderedCancelAddMonoid Γ] →
            [inst : CommRing R] →
              [inst_2 : CommRing V] → [Algebra R V] → HahnSeries Γ V → PowerSeries R → HahnSeries.SummableFamily Γ V ℕ
-- Aesop.Frontend.Attribute
Aesop.Frontend.instInhabitedAttrConfig : Inhabited Aesop.Frontend.AttrConfig
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
instDiscreteMeasurableSpace : ∀ {α : Type u_1}, DiscreteMeasurableSpace α
-- Mathlib.Order.MinMax
max_le_max_right : ∀ {α : Type u} [inst : LinearOrder α] {a b : α} (c : α), a ≤ b → max a c ≤ max b c
-- Mathlib.Data.Finset.Prod
Finset.image_diag : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (f : α × α → β) (s : Finset α),
  Finset.image f s.diag = Finset.image (fun x => f (x, x)) s
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.color : Lean.Lsp.CompletionItemKind
-- Mathlib.CategoryTheory.Adjunction.Reflective
/-- If `i` has a reflector `L`, then the function `(i.obj (L.obj A) ⟶ B) → (A ⟶ B)` given by
precomposing with `η.app A` is a bijection provided `B` is in the essential image of `i`.
That is, the function `fun (f : i.obj (L.obj A) ⟶ B) ↦ η.app A ≫ f` is bijective,
as long as `B` is in the essential image of `i`.
This definition gives an equivalence: the key property that the inverse can be described
nicely is shown in `unitCompPartialBijective_symm_apply`.

This establishes there is a natural bijection `(A ⟶ B) ≃ (i.obj (L.obj A) ⟶ B)`. In other words,
from the point of view of objects in `D`, `A` and `i.obj (L.obj A)` look the same: specifically
that `η.app A` is an isomorphism.
 -/
CategoryTheory.unitCompPartialBijective : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {i : CategoryTheory.Functor D C} →
          [inst_2 : CategoryTheory.Reflective i] →
            (A : C) → {B : C} → i.essImage B → (A ⟶ B) ≃ (i.obj ((CategoryTheory.reflector i).obj A) ⟶ B)
-- Mathlib.Algebra.Polynomial.Smeval
Polynomial.smeval_at_zero : ∀ (R : Type u_1) [inst : Semiring R] (p : Polynomial R) {S : Type u_2} [inst_1 : NonAssocSemiring S]
  [inst_2 : Module R S] [inst_3 : Pow S ℕ] [NatPowAssoc S], p.smeval 0 = p.coeff 0 • 1
-- Mathlib.LinearAlgebra.Quotient.Defs
Submodule.Quotient.module : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Ring R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (P : Submodule R M) → Module R (M ⧸ P)
-- Mathlib.Topology.Algebra.Group.Defs
IsTopologicalAddGroup.toContinuousAdd : ∀ {G : Type u} {inst : TopologicalSpace G} {inst_1 : AddGroup G} [self : IsTopologicalAddGroup G], ContinuousAdd G
-- Mathlib.Tactic.Abel
_private.Mathlib.Tactic.Abel.0.Mathlib.Tactic.Abel.instEvalExprConfig : Lean.Elab.ConfigEval.EvalExpr Mathlib.Tactic.AtomM.Recurse.Config
-- Mathlib.RingTheory.HahnSeries.Lex
HahnSeries.embDomainOrderAddMonoidHom_injective : ∀ {Γ : Type u_1} {R : Type u_2} [inst : LinearOrder Γ] [inst_1 : PartialOrder R] {Γ' : Type u_3}
  [inst_2 : LinearOrder Γ'] (f : Γ ↪o Γ') [inst_3 : AddMonoid R],
  Function.Injective ⇑(HahnSeries.embDomainOrderAddMonoidHom f)
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.hsum_smul_module : ∀ {Γ : Type u_1} {Γ' : Type u_2} {α : Type u_5} [inst : PartialOrder Γ] [inst_1 : PartialOrder Γ'] [inst_2 : VAdd Γ Γ']
  [inst_3 : IsOrderedCancelVAdd Γ Γ'] {R : Type u_7} {V : Type u_8} [inst_4 : Semiring R] [inst_5 : AddCommMonoid V]
  [inst_6 : Module R V] {x : HahnSeries Γ R} {s : HahnSeries.SummableFamily Γ' V α},
  (x • s).hsum = (HahnModule.of R).symm (x • (HahnModule.of R) s.hsum)
-- Mathlib.Algebra.Polynomial.UnitTrinomial
Polynomial.trinomial_trailingCoeff : ∀ {R : Type u_1} [inst : Semiring R] {k m n : ℕ} {u v w : R},
  k < m → m < n → u ≠ 0 → (Polynomial.trinomial k m n u v w).trailingCoeff = u
-- Init.Data.Option.Monadic
Option.forIn'_none : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [inst : Monad m] (b : β)
  (f : (a : α) → a ∈ none → β → m (ForInStep β)), forIn' none b f = pure b
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Path.ins.eq_5 : ∀ {α : Type u_1} (x a : RBTree.RBNode α) (y : α) (parent : RBTree.RBNode.Path α),
  (RBTree.RBNode.Path.right RBTree.RBColor.black a y parent).ins x = parent.ins (a.balance2 y x)
-- Mathlib.Topology.Order.OrderClosed
Ioo_mem_nhdsLE_of_mem : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIicTopology α] {a b c : α},
  b ∈ Set.Ioo a c → Set.Ioo a c ∈ nhdsWithin b (Set.Iic b)
-- Mathlib.Data.Multiset.Find
_private.Mathlib.Data.Multiset.Find.0.List.filter.match_1.splitter : (motive : Bool → Sort u_1) → (x : Bool) → (Unit → motive true) → (Unit → motive false) → motive x
-- Mathlib.CategoryTheory.Abelian.Projective.Extend
CategoryTheory.ProjectiveResolution.Hom.hom'.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X : C}
  {R : CategoryTheory.ProjectiveResolution X} {X' : C} {R' : CategoryTheory.ProjectiveResolution X'} {f : X ⟶ X'}
  (φ : R.Hom R' f), φ.hom' = HomologicalComplex.extendMap φ.hom ComplexShape.embeddingDownNat
-- Mathlib.Topology.Basic
Classical.strongIndefiniteDescription.eq_1 : ∀ {α : Sort u} (p : α → Prop) (h : Nonempty α),
  Classical.strongIndefiniteDescription p h =
    if hp : ∃ x, p x then
      have this :=
        let xp := Classical.indefiniteDescription p hp;
        ⟨↑xp, ⋯⟩;
      this
    else ⟨Classical.choice h, ⋯⟩
-- Init.Data.Range.Polymorphic.Iterators
Std.Ric.instForIn'InferInstanceMembershipOfLawfulUpwardEnumerableOfLawfulUpwardEnumerableLEOfLawfulUpwardEnumerableLeast?OfMonadOfFiniteIteratorId : {α : Type u} →
  {m : Type u → Type u_1} →
    [inst : Std.PRange.UpwardEnumerable α] →
      [inst_1 : LE α] →
        [inst_2 : DecidableLE α] →
          [inst_3 : Std.PRange.Least? α] →
            [Std.PRange.LawfulUpwardEnumerable α] →
              [Std.PRange.LawfulUpwardEnumerableLE α] →
                [Std.PRange.LawfulUpwardEnumerableLeast? α] →
                  [Monad m] → [Std.Iterators.Finite (Std.Rxc.Iterator α) Id] → ForIn' m (Std.Ric α) α inferInstance
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.CustomEliminators.mk.inj : ∀ {map map_1 : Lean.SMap (Bool × Array Lean.Name) Lean.Name}, { map := map } = { map := map_1 } → map = map_1
-- Mathlib.Dynamics.Flow
/-- **Alias** of `Flow.continuous`. -/
Continuous.flow : ∀ {τ : Type u_1} {α : Type u_2} [inst : TopologicalSpace τ] [inst_1 : TopologicalSpace α] [inst_2 : AddZero τ]
  (ϕ : Flow τ α) {β : Type u_3} [inst_3 : TopologicalSpace β] {t : β → τ},
  Continuous t → ∀ {f : β → α}, Continuous f → Continuous fun x => ϕ.toFun (t x) (f x)
-- Init.Data.List.Perm
List.Perm.append_right : ∀ {α : Type u_1} {l₁ l₂ : List α} (t₁ : List α), l₁.Perm l₂ → (l₁ ++ t₁).Perm (l₂ ++ t₁)
-- Batteries.Data.List.Pairwise
List.pairwise_iff_get : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α},
  List.Pairwise R l ↔ ∀ (i j : Fin l.length), i < j → R (l.get i) (l.get j)
-- Batteries.Data.String.Legacy
_private.Batteries.Data.String.Legacy.0.String.utf8ByteSize'.go.eq_def : ∀ (a : List Char),
  String.utf8ByteSize'.go✝ a =
    match a with
    | [] => 0
    | c :: cs => String.utf8ByteSize'.go✝ cs + c.utf8Size
-- Std.Http.Data.Body.Stream
/-- Whether the channel is closed.
 -/
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Channel.State.closed : Std.Http.Body.Channel.State✝ → Bool
-- Mathlib.Data.Nat.ModEq
Nat.chineseRemainder_modEq_unique : ∀ {m n : ℕ} (co : n.Coprime m) {a b z : ℕ},
  z ≡ a [MOD n] → z ≡ b [MOD m] → z ≡ ↑(Nat.chineseRemainder co a b) [MOD n * m]
-- Init.Grind.Config
Lean.Grind.GrobnerConfig.mk.sizeOf_spec : ∀ (toNoopConfig : Lean.Grind.NoopConfig), sizeOf { toNoopConfig := toNoopConfig } = 1 + sizeOf toNoopConfig
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- **Alias** of `add_apply`. -/
ContinuousLinearMap.add_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Add β}
  {inst_2 : Add F} [self : IsAddApply F α β] (f g : F) (x : α), (f + g) x = f x + g x
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintInfo.kind? : Lean.Elab.InlayHintInfo → Option Lean.Elab.InlayHintKind
-- Mathlib.CategoryTheory.Triangulated.Generators
CategoryTheory.ObjectProperty.triangEnvelopeIter.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) (n : ℕ),
  P.triangEnvelopeIter n =
    ((P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter n).retractClosure
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Matrix.charmatrix_fromBlocks : ∀ {R : Type u_1} [inst : CommRing R] {m : Type u_3} {n : Type u_4} [inst_1 : DecidableEq m] [inst_2 : DecidableEq n]
  [inst_3 : Fintype m] [inst_4 : Fintype n] (M₁₁ : Matrix m m R) (M₁₂ : Matrix m n R) (M₂₁ : Matrix n m R)
  (M₂₂ : Matrix n n R),
  (Matrix.fromBlocks M₁₁ M₁₂ M₂₁ M₂₂).charmatrix =
    Matrix.fromBlocks M₁₁.charmatrix (-M₁₂.map ⇑Polynomial.C) (-M₂₁.map ⇑Polynomial.C) M₂₂.charmatrix
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.IsUniversal.top : ∀ {V : Type u} {v : V}, ⊤.IsUniversal v
-- Mathlib.GroupTheory.Complement
AddSubgroup.isComplement_singleton_left : ∀ {G : Type u_1} [inst : AddGroup G] {S : Set G} {g : G}, AddSubgroup.IsComplement {g} S ↔ S = Set.univ
-- Init.PropLemmas
Bool.ite_else_false_eq_false : ∀ {p : Prop} [inst : Decidable p] {x : Bool}, (if p then x else false) = false ↔ ¬p ∨ x = false
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_domSMul : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {G : Type u_6} {A : Type u_7}
  [inst_2 : Group G] [inst_3 : AddCommGroup A] [inst_4 : DistribMulAction G A] [inst_5 : MeasurableSpace A]
  [inst_6 : MeasurableConstSMul G A] {μ : MeasureTheory.Measure A} (g : Gᵈᵐᵃ) (f : A → E),
  ∫ (x : A), f x ∂g • μ = ∫ (x : A), f ((DomMulAct.mk.symm g)⁻¹ • x) ∂μ
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.norm_exponent_zero : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  (f : ↥(MeasureTheory.Lp E 0 μ)), ‖f‖ = 0
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Cont'.fix.sizeOf_spec : ∀ (a : Turing.ToPartrec.Code) (a_1 : Turing.PartrecToTM2.Cont'),
  sizeOf (Turing.PartrecToTM2.Cont'.fix a a_1) = 1 + sizeOf a + sizeOf a_1
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.lintegral_deterministic' : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : β → ENNReal} {g : α → β} {a : α}
  (hg : Measurable g), Measurable f → ∫⁻ (x : β), f x ∂(ProbabilityTheory.Kernel.deterministic g hg) a = f (g a)
-- Mathlib.ModelTheory.LanguageMap
/-- A language homomorphism maps the symbols of one language to symbols of another.  -/
FirstOrder.Language.LHom : FirstOrder.Language → FirstOrder.Language → Type (max (max (max u u') v) v')
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionCommRingCatFSheafedSpaceToSheafedSpaceGlueDataToLocallyRingedSpaceGlueData : ∀ (D : AlgebraicGeometry.Scheme.GlueData) (i j : D.J),
  AlgebraicGeometry.SheafedSpace.IsOpenImmersion (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.f i j)
-- Mathlib.Analysis.Normed.Operator.Prod
/-- The operator norm of the first projection `E × F → E` is exactly 1 if `E` is nontrivial.  -/
ContinuousLinearMap.norm_fst : ∀ (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [Nontrivial E],
  ‖ContinuousLinearMap.fst 𝕜 E F‖ = 1
-- Init.GrindInstances.ToInt
Lean.Grind.instZeroInt64SintOfNatNat : Lean.Grind.ToInt.Zero Int64 (Lean.Grind.IntInterval.sint 64)
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.one_plus_not_eq_not_plus_one : ∀ {w : ℕ} (x : BitVec w), 1#w + ~~~x = ~~~x + 1#w