mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
CategoryTheory.Presheaf.instPreservesFiniteProductsOppositeObjFunctorIsSheafCoherentTopology : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u₃}
  [inst_1 : CategoryTheory.Category.{v₃, u₃} A] [inst_2 : CategoryTheory.Preregular C]
  [inst_3 : CategoryTheory.FinitaryExtensive C] (F : CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) A),
  CategoryTheory.Limits.PreservesFiniteProducts F.obj
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
/-- If `c` is a pullback cone in `Cᵒᵖ`, then `c.unop.op` is isomorphic to `c`.  -/
CategoryTheory.Limits.PullbackCone.unopOpIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y Z : Cᵒᵖ} → {f : X ⟶ Z} → {g : Y ⟶ Z} → (c : CategoryTheory.Limits.PullbackCone f g) → c.unop.op ≅ c
-- Mathlib.Order.SuccPred.Basic
Order.Iic_pred_of_not_isMin : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] {a : α}, ¬IsMin a → Set.Iic (Order.pred a) = Set.Iio a
-- Std.Sat.AIG.LawfulVecOperator
Std.Sat.AIG.LawfulVecOperator.le_size_of_le_aig_size : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {β : Std.Sat.AIG α → ℕ → Type}
  {f : {len : ℕ} → (aig : Std.Sat.AIG α) → β aig len → Std.Sat.AIG.RefVecEntry α len}
  [Std.Sat.AIG.LawfulVecOperator α β fun {len} => f] {len x : ℕ} (aig : Std.Sat.AIG α) (input : β aig len),
  x ≤ aig.decls.size → x ≤ (f aig input).aig.decls.size
-- Lean.Elab.InfoTree.Types
Lean.Elab.ContextInfo.mk.sizeOf_spec : ∀ (toCommandContextInfo : Lean.Elab.CommandContextInfo) (parentDecl? : Option Lean.Name)
  (autoImplicits : Array Lean.Expr),
  sizeOf { toCommandContextInfo := toCommandContextInfo, parentDecl? := parentDecl?, autoImplicits := autoImplicits } =
    1 + sizeOf toCommandContextInfo + sizeOf parentDecl? + sizeOf autoImplicits
-- Mathlib.Order.Hom.Basic
OrderIso.coe_dualDual : ∀ (α : Type u_2) [inst : LE α], ⇑(OrderIso.dualDual α) = ⇑OrderDual.toDual ∘ ⇑OrderDual.toDual
-- Mathlib.CategoryTheory.Sites.Point.Skyscraper
/-- If `Φ` is a point of a site `(C, J)`, `P : Cᵒᵖ ⥤ A` and `M : A`, this is
the bijection `(Φ.presheafFiber.obj P ⟶ M) ≃ (P ⟶ Φ.skyscraperPresheaf M)`
that is part of the adjunction `skyscraperPresheafAdjunction`.  -/
CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      (Φ : J.Point) →
        {A : Type u'} →
          [inst_1 : CategoryTheory.Category.{v', u'} A] →
            [inst_2 : CategoryTheory.Limits.HasProducts A] →
              {P : CategoryTheory.Functor Cᵒᵖ A} →
                {M : A} →
                  [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] →
                    (Φ.presheafFiber.obj P ⟶ M) ≃ (P ⟶ Φ.skyscraperPresheaf M)
-- Init.Data.Nat.Basic
Nat.le_of_add_left_le : ∀ {n m k : ℕ}, k + n ≤ m → n ≤ m
-- Mathlib.Data.Real.Pointwise
Real.smul_iSup_of_nonneg : ∀ {ι : Sort u_1} {α : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : MulActionWithZero α ℝ] [IsOrderedModule α ℝ] {a : α}, 0 ≤ a → ∀ (f : ι → ℝ), a • ⨆ i, f i = ⨆ i, a • f i
-- Mathlib.Order.Lattice
sup_inf_left : ∀ {α : Type u} [inst : DistribLattice α] (a b c : α), a ⊔ b ⊓ c = (a ⊔ b) ⊓ (a ⊔ c)
-- Std.Internal.Do.PredTrans
/-- Unfolding `ite` through `apply`.  -/
Std.Internal.Do.PredTrans.apply_ite : ∀ {α : Type u_1} {Pred : Type u} {EPred : Type v} (c : Prop) [inst : Decidable c]
  (t e : Std.Internal.Do.PredTrans Pred EPred α) (post : α → Pred) (epost : EPred),
  (if c then t else e).apply post epost = if c then t.apply post epost else e.apply post epost
-- Mathlib.Order.SuccPred.Basic
Order.lt_succ_iff_of_not_isMax' : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] {a b : α}, ¬IsMax b → (b < Order.succ a ↔ b ≤ a)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey_eq_getKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {a fallback : α}
  {h : a ∈ t}, t.getKey a h = t.getKeyD a fallback
-- Mathlib.RingTheory.Ideal.Lattice
Ideal.mem_iSup_of_mem : ∀ {R : Type u} [inst : Semiring R] {ι : Sort u_1} {S : ι → Ideal R} (i : ι) {x : R}, x ∈ S i → x ∈ iSup S
-- Mathlib.Topology.Instances.Real.Lemmas
Real.mem_closure_iff : ∀ {s : Set ℝ} {x : ℝ}, x ∈ closure s ↔ ∀ ε > 0, ∃ y ∈ s, |y - x| < ε
-- Mathlib.CategoryTheory.Retract
/-- If a morphism `f` in the opposite category is a retract of `g`,
then `f.unop` is a retract of `g.unop`.  -/
CategoryTheory.RetractArrow.unop : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z W : Cᵒᵖ} →
      {f : X ⟶ Y} → {g : Z ⟶ W} → CategoryTheory.RetractArrow f g → CategoryTheory.RetractArrow f.unop g.unop
-- Mathlib.Tactic.MinImports
/-- Returns `true` if `n` is `Init` or a descendant of `Init`. These imports are always available
in ordinary Mathlib files, so they are omitted from user-facing `#min_imports` output.  -/
Mathlib.Command.MinImports.isInitImport : Lean.Name → Bool
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.union.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (m₁ m₁_1 : Std.ExtDTreeMap α β cmp),
  m₁ = m₁_1 → ∀ (m₂ m₂_1 : Std.ExtDTreeMap α β cmp), m₂ = m₂_1 → m₁.union m₂ = m₁_1.union m₂_1
-- Mathlib.AlgebraicTopology.ModelCategory.Basic
HomotopicalAlgebra.ModelCategory.instIsWeakFactorizationSystemTrivialCofibrationsFibrations : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C],
  (HomotopicalAlgebra.trivialCofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.fibrations C)
-- Aesop.Forward.Substitution
Aesop.instInhabitedSubstitution : Inhabited Aesop.Substitution
-- Mathlib.Algebra.Lie.Prod
LieAlgebra.Prod.instLieAlgebra : {R : Type u_1} →
  {L₁ : Type u_2} →
    {L₂ : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : LieRing L₁] → [LieAlgebra R L₁] → [inst_3 : LieRing L₂] → [LieAlgebra R L₂] → LieAlgebra R (L₁ × L₂)
-- Mathlib.LinearAlgebra.Span.Defs
LinearEquiv.isPrincipal_iff : ∀ {R : Type u_1} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M₂] (e : M ≃ₗ[R] M₂), Module.IsPrincipal R M ↔ Module.IsPrincipal R M₂
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PrepathObject.ι_p₁_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (self : HomotopicalAlgebra.PrepathObject A) {Z : C}
  (h : A ⟶ Z), CategoryTheory.CategoryStruct.comp self.ι (CategoryTheory.CategoryStruct.comp self.p₁ h) = h
-- Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
Algebra.Generators.cotangentCompLocalizationAwayEquiv_symm_comp_inl : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} {ι : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T] (g : S) [inst_7 : IsLocalization.Away g T] (P : Algebra.Generators R S ι)
  {x : ((Algebra.Generators.localizationAway T g).comp P).toExtension.Cotangent}
  (hx :
    (Algebra.Extension.Cotangent.map ((Algebra.Generators.localizationAway T g).ofComp P).toExtensionHom) x =
      Algebra.Generators.cMulXSubOneCotangent T g),
  ↑(Algebra.Generators.cotangentCompLocalizationAwayEquiv g P hx).symm ∘ₗ
      LinearMap.inl T (TensorProduct S T P.toExtension.Cotangent)
        (Algebra.Generators.localizationAway T g).toExtension.Cotangent =
    LinearMap.liftBaseChange T
      (Algebra.Extension.Cotangent.map ((Algebra.Generators.localizationAway T g).toComp P).toExtensionHom)
-- Mathlib.Data.Set.Monotone
StrictAntiOn.strictAnti : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β],
  StrictAntiOn f s → StrictAnti (f ∘ Subtype.val)
-- Mathlib.NumberTheory.DirichletCharacter.Bounds
/-- The value at a unit of a Dirichlet character with target a normed field has norm `1`.  -/
DirichletCharacter.unit_norm_eq_one : ∀ {F : Type u_1} [inst : NormedField F] {n : ℕ} (χ : DirichletCharacter F n) (a : (ZMod n)ˣ), ‖χ ↑a‖ = 1
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.closure_prod : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {s : Set G} {t : Set N},
  0 ∈ s → 0 ∈ t → AddSubgroup.closure (s ×ˢ t) = (AddSubgroup.closure s).prod (AddSubgroup.closure t)
-- Mathlib.FieldTheory.IsAlgClosed.Basic
IsAlgClosed.roots_eq_zero_iff : ∀ {k : Type u} [inst : Field k] [IsAlgClosed k] {p : Polynomial k}, p.roots = 0 ↔ p = Polynomial.C (p.coeff 0)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKeyD_union_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : α → Type v} {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k fallback : α}, k ∉ m₁ → (m₁ ∪ m₂).getKeyD k fallback = m₂.getKeyD k fallback
-- Lean.Meta.Tactic.Ext
/-- Erased `ext`s via `attribute [-ext]`.  -/
Lean.Meta.Ext.ExtTheorems.erased : Lean.Meta.Ext.ExtTheorems → Lean.PHashSet Lean.Name
-- Mathlib.CategoryTheory.Monoidal.Internal.Types.CommGrp_
/-- The equivalences `Grp (Type u) ≌ GrpCat.{u}` and `CommGrp (Type u) ≌ CommGrpCat.{u}`
are naturally compatible with the forgetful functors to `GrpCat` and `Grp (Type u)`.
 -/
commGrpTypeEquivalenceCommGrpForgetGrp : CommGrpTypeEquivalenceCommGrp.functor.comp (CategoryTheory.forget₂ CommGrpCat GrpCat) ≅
  (CategoryTheory.CommGrp.forget₂Grp (Type u)).comp GrpTypeEquivalenceGrp.functor
-- Mathlib.LinearAlgebra.Matrix.Vec
Matrix.star_vec_dotProduct_vec : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_1} [inst : AddCommMonoid R] [inst_1 : Mul R] [inst_2 : Star R]
  [inst_3 : Fintype m] [inst_4 : Fintype n] (A B : Matrix m n R), star A.vec ⬝ᵥ B.vec = (A.conjTranspose * B).trace
-- Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Ideal.radical_minimalPrimes : ∀ {R : Type u_1} [inst : CommSemiring R] {I : Ideal R}, I.radical.minimalPrimes = I.minimalPrimes
-- Mathlib.GroupTheory.Coset.Basic
/-- If `H ≤ K`, then `G/H ≃ G/K × K/H` nonconstructively. The
constructive version is `quotientEquivProdOfLE'`.  -/
AddSubgroup.quotientEquivProdOfLE : {α : Type u_1} → [inst : AddGroup α] → {s t : AddSubgroup α} → s ≤ t → α ⧸ s ≃ (α ⧸ t) × ↥t ⧸ s.addSubgroupOf t
-- Mathlib.Topology.DiscreteSubset
Set.Subsingleton.isDiscrete : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, s.Subsingleton → IsDiscrete s
-- Mathlib.Topology.Compactness.Lindelof
/-- The complement to a Lindelöf set belongs to a filter `f` with the countable intersection
property if it belongs to each filter `𝓝 x ⊓ f`, `x ∈ s`.  -/
IsLindelof.compl_mem_sets : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  IsLindelof s → ∀ {f : Filter X} [CountableInterFilter f], (∀ x ∈ s, sᶜ ∈ nhds x ⊓ f) → sᶜ ∈ f
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.toPoly'.go.eq_def : ∀ (coeff : ℤ) (a : Int.Internal.Linear.Expr),
  Int.Internal.Linear.Expr.toPoly'.go coeff a =
    match (motive := Int.Internal.Linear.Expr → Int.Internal.Linear.Poly → Int.Internal.Linear.Poly) a with
    | Int.Internal.Linear.Expr.num k => bif k == 0 then id else fun x => x.addConst (coeff.mul k)
    | Int.Internal.Linear.Expr.var v => fun x => Int.Internal.Linear.Poly.add coeff v x
    | a.add b => Int.Internal.Linear.Expr.toPoly'.go coeff a ∘ Int.Internal.Linear.Expr.toPoly'.go coeff b
    | a.sub b => Int.Internal.Linear.Expr.toPoly'.go coeff a ∘ Int.Internal.Linear.Expr.toPoly'.go (-coeff) b
    | Int.Internal.Linear.Expr.mulL k a => bif k == 0 then id else Int.Internal.Linear.Expr.toPoly'.go (coeff.mul k) a
    | a.mulR k => bif k == 0 then id else Int.Internal.Linear.Expr.toPoly'.go (coeff.mul k) a
    | a.neg => Int.Internal.Linear.Expr.toPoly'.go (-coeff) a
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.unreach.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (type type_1 : Lean.Expr),
  (Lean.Compiler.LCNF.Code.unreach type = Lean.Compiler.LCNF.Code.unreach type_1) = (type = type_1)
-- Mathlib.Topology.Algebra.AsymptoticCone
/-- The set of directions `v` for which the set has points arbitrarily far in directions near `v`.
 -/
asymptoticCone : (k : Type u_1) →
  {V : Type u_2} →
    {P : Type u_3} →
      [inst : Field k] →
        [LinearOrder k] →
          [inst_2 : AddCommGroup V] → [Module k V] → [AddTorsor V P] → [TopologicalSpace V] → Set P → Set V
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.mem_fixedPoints' : ∀ {M : Type u_1} {α : Type u_3} [inst : Monoid M] [inst_1 : MulAction M α] {a : α},
  a ∈ MulAction.fixedPoints M α ↔ ∀ a' ∈ MulAction.orbit M a, a' = a
-- Mathlib.Order.Filter.AtTopBot.Finite
/-- Given an antitone basis `s : ℕ → Set α` of a filter, extract an antitone subbasis `s ∘ φ`,
`φ : ℕ → ℕ`, such that `m < n` implies `r (φ m) (φ n)`. This lemma can be used to extract an
antitone basis with basis sets decreasing "sufficiently fast".  -/
Filter.HasAntitoneBasis.subbasis_with_rel : ∀ {α : Type u_3} {f : Filter α} {s : ℕ → Set α},
  f.HasAntitoneBasis s →
    ∀ {r : ℕ → ℕ → Prop},
      (∀ (m : ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, r m n) →
        ∃ φ, StrictMono φ ∧ (∀ ⦃m n : ℕ⦄, m < n → r (φ m) (φ n)) ∧ f.HasAntitoneBasis (s ∘ φ)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
/-- A subgraph is called an *induced subgraph* if vertices of `G'` are adjacent if
they are adjacent in `G`.  -/
SimpleGraph.Subgraph.IsInduced : {V : Type u} → {G : SimpleGraph V} → G.Subgraph → Prop
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.mk'_smul : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  [inst_5 : IsLocalizedModule S f] {R₀ : Type u_6} [inst_6 : SMul R₀ R] [inst_7 : SMul R₀ M] [inst_8 : SMul R₀ M']
  [IsScalarTower R₀ R R] [IsScalarTower R₀ R M] [IsScalarTower R₀ R M'] (r : R₀) (m : M) (s : ↥S),
  IsLocalizedModule.mk' f (r • m) s = r • IsLocalizedModule.mk' f m s
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Zipper.toList : {α : Type u} → {β : α → Type v} → Std.DTreeMap.Internal.Zipper α β → List ((a : α) × β a)
-- Mathlib.Tactic.Rify
Mathlib.Tactic.Rify.ratCast_eq : ∀ (a b : ℚ), a = b ↔ ↑a = ↑b
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.rightHomologyMap'_op : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData),
  (CategoryTheory.ShortComplex.rightHomologyMap' φ h₁ h₂).op =
    CategoryTheory.ShortComplex.leftHomologyMap' (CategoryTheory.ShortComplex.opMap φ) h₂.op h₁.op
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.eq_of_xn_modEq_lem1 : ∀ {a : ℕ} (a1 : 1 < a) {i n j : ℕ}, i < j → j < n → Pell.xn a1 i % Pell.xn a1 n < Pell.xn a1 j % Pell.xn a1 n
-- Mathlib.Analysis.Meromorphic.Divisor
/-- If orders are finite, the divisor of the product of two meromorphic functions is the sum of the
divisors.
 -/
MeromorphicOn.divisor_fun_mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {U : Set 𝕜} {f₁ f₂ : 𝕜 → 𝕜},
  MeromorphicOn f₁ U →
    MeromorphicOn f₂ U →
      (∀ z ∈ U, meromorphicOrderAt f₁ z ≠ ⊤) →
        (∀ z ∈ U, meromorphicOrderAt f₂ z ≠ ⊤) →
          MeromorphicOn.divisor (fun z => f₁ z * f₂ z) U = MeromorphicOn.divisor f₁ U + MeromorphicOn.divisor f₂ U
-- Init.Data.Rat.Lemmas
Rat.num_natCast : ∀ (n : ℕ), (↑n).num = ↑n
-- Mathlib.Data.Multiset.DershowitzManna
_private.Mathlib.Data.Multiset.DershowitzManna.0.Multiset.isDershowitzMannaLT_of_transGen_oneStep : ∀ {α : Type u_1} [inst : Preorder α] {M N : Multiset α},
  Relation.TransGen Multiset.OneStep✝ M N → M.IsDershowitzMannaLT N
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.piecewise_univ : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] (f g : MeasureTheory.SimpleFunc α β),
  MeasureTheory.SimpleFunc.piecewise Set.univ ⋯ f g = f
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get!_alter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k k' : α} [hi : Inhabited (β k')] {f : Option (β k) → Option (β k)},
  m.WF → (m.alter k f).get! k' = if heq : (k == k') = true then (Option.map (cast ⋯) (f (m.get? k))).get! else m.get! k'
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.equiv_mul_right : ∀ {G : Type u_1} [inst : Group G] {K : Subgroup G} {S : Set G} (hSK : Subgroup.IsComplement S ↑K) (g : G) (k : ↥K),
  hSK.equiv (g * ↑k) = ((hSK.equiv g).1, (hSK.equiv g).2 * k)
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.coe_mk' : ∀ {𝕜 : Type u_1} {V₁ : Type u_3} {V₂ : Type u_5} {P₁ : Type u_8} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V₁] [inst_2 : NormedSpace 𝕜 V₁] [inst_3 : PseudoMetricSpace P₁]
  [inst_4 : NormedAddTorsor V₁ P₁] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (e : P₁ → P₂) (e' : V₁ ≃ₗᵢ[𝕜] V₂) (p : P₁)
  (h : ∀ (p' : P₁), e p' = e' (p' -ᵥ p) +ᵥ e p), ⇑(AffineIsometryEquiv.mk' e e' p h) = e
-- Init.Data.Int.Linear
/-- `p.mul k` multiplies all coefficients and constant of the polynomial `p` by `k`.
 -/
Int.Internal.Linear.Poly.mul' : Int.Internal.Linear.Poly → ℤ → Int.Internal.Linear.Poly
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.NumDenSameDeg.den_neg : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : NegMemClass σ A]
  {𝒜 : ι → σ} (x : Submonoid A) (c : HomogeneousLocalization.NumDenSameDeg 𝒜 x), ↑(-c).den = ↑c.den
-- Mathlib.Data.Nat.Squarefree
Nat.sq_mul_squarefree_of_pos' : ∀ {n : ℕ}, 0 < n → ∃ a b, (b + 1) ^ 2 * (a + 1) = n ∧ Squarefree (a + 1)
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.distortion_le_of_mem : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) [inst : Fintype ι],
  J ∈ π → J.distortion ≤ π.distortion
-- Mathlib.Algebra.Lie.Subalgebra
/-- The zero algebra is a subalgebra of any Lie algebra.  -/
instZeroLieSubalgebra : (R : Type u) →
  (L : Type v) → [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → Zero (LieSubalgebra R L)
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.LeftExtension.postcompose₂_obj_hom_app : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H)
  (G : CategoryTheory.Functor H D')
  (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.Functor.whiskeringLeft C D H).obj L))
  (X_1 : C), ((CategoryTheory.Functor.LeftExtension.postcompose₂ L F G).obj X).hom.app X_1 = G.map (X.hom.app X_1)
-- Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes
Mathlib.Tactic.Bicategory.structuralIsoOfExpr_whiskerRight : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f g : a ⟶ b} (h : b ⟶ c) (η : f ⟶ g) (η' : f ≅ g),
  η'.hom = η → (CategoryTheory.Bicategory.whiskerRightIso η' h).hom = CategoryTheory.Bicategory.whiskerRight η h
-- Mathlib.Analysis.LocallyConvex.WeakSpace
/-- If `e` is a linear isomorphism between two locally convex spaces, and `e` induces (via
precomposition) an isomorphism between their continuous duals, then `e` commutes with the closure
on convex sets.

The hypotheses hold automatically for `e := toWeakSpace 𝕜 E`, see `Convex.toWeakSpace_closure`.  -/
LinearEquiv.image_closure_of_convex : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : AddCommGroup F] [inst_4 : Module 𝕜 F] [inst_5 : Module ℝ E] [IsScalarTower ℝ 𝕜 E] [inst_7 : Module ℝ F]
  [IsScalarTower ℝ 𝕜 F] [inst_9 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E]
  [LocallyConvexSpace ℝ E] [inst_13 : TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F]
  [LocallyConvexSpace ℝ F] {s : Set E},
  Convex ℝ s →
    ∀ (e : E ≃ₗ[𝕜] F),
      (∀ (f : StrongDual 𝕜 F), Continuous ⇑(e.dualMap ↑f)) →
        (∀ (f : StrongDual 𝕜 E), Continuous ⇑(e.symm.dualMap ↑f)) → ⇑e '' closure s = closure (⇑e '' s)
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.mono_g : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C}, S.Exact → S.f = 0 → CategoryTheory.Mono S.g
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.sign_signedInfDist_lineMap_incenter_touchpoint : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) {i j : Fin (n + 1)},
  i ≠ j →
    ∀ {r : ℝ},
      r ∈ Set.Icc 0 1 →
        SignType.sign ((s.signedInfDist j) ((AffineMap.lineMap s.incenter (s.touchpoint ∅ i)) r)) =
          SignType.sign ((s.signedInfDist j) s.incenter)
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.Quotient.natTransLift_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (r : HomRel C) {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor (CategoryTheory.Quotient r) D),
  CategoryTheory.Quotient.natTransLift r
      (CategoryTheory.CategoryStruct.id ((CategoryTheory.Quotient.functor r).comp F)) =
    CategoryTheory.CategoryStruct.id F
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Bicones.functoriality_obj_pt : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {D : Type uD} [inst_2 : CategoryTheory.Category.{uD', uD} D]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (F : J → C) (G : CategoryTheory.Functor C D)
  [inst_4 : G.PreservesZeroMorphisms] (A : CategoryTheory.Limits.Bicone F),
  ((CategoryTheory.Limits.Bicones.functoriality F G).obj A).pt = G.obj A.pt
-- Aesop.Search.Queue
Aesop.BestFirstQueue.ActiveGoal.mk : Aesop.GoalRef → Aesop.Percent → Aesop.Iteration → Aesop.Iteration → Aesop.BestFirstQueue.ActiveGoal
-- Mathlib.Algebra.Module.Submodule.Defs
/-- This can't be an instance because Lean wouldn't know how to find `R`, but we can still use
this to manually derive `Module` on specific types.  -/
SMulMemClass.toModule' : (S : Type u_2) →
  (R' : Type u_3) →
    (R : Type u_4) →
      (A : Type u_5) →
        [inst : Semiring R] →
          [inst_1 : NonUnitalNonAssocSemiring A] →
            [inst_2 : Module R A] →
              [inst_3 : Semiring R'] →
                [inst_4 : SMul R' R] →
                  [inst_5 : Module R' A] →
                    [IsScalarTower R' R A] →
                      [inst_7 : SetLike S A] →
                        [inst_8 : AddSubmonoidClass S A] → [SMulMemClass S R A] → (s : S) → Module R' ↥s
-- Mathlib.Analysis.Calculus.LHopital
deriv.lhopital_zero_right_on_Ico : ∀ {a b : ℝ} {l : Filter ℝ} {f g : ℝ → ℝ},
  a < b →
    DifferentiableOn ℝ f (Set.Ioo a b) →
      ContinuousOn f (Set.Ico a b) →
        ContinuousOn g (Set.Ico a b) →
          (∀ x ∈ Set.Ioo a b, deriv g x ≠ 0) →
            f a = 0 →
              g a = 0 →
                Filter.Tendsto (fun x => deriv f x / deriv g x) (nhdsWithin a (Set.Ioi a)) l →
                  Filter.Tendsto (fun x => f x / g x) (nhdsWithin a (Set.Ioi a)) l
-- Mathlib.Topology.Algebra.AsymptoticCone
asymptoticCone_asymptoticCone : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [inst_4 : AddTorsor V P] [inst_5 : TopologicalSpace V] [inst_6 : TopologicalSpace k]
  [OrderTopology k] [IsStrictOrderedRing k] [IsTopologicalAddGroup V] [ContinuousSMul k V] (s : Set P),
  asymptoticCone k (asymptoticCone k s) = asymptoticCone k s
-- Mathlib.RingTheory.PowerSeries.Inverse
PowerSeries.isUnit_iff_constantCoeff : ∀ {R : Type u_1} [inst : Ring R] {φ : PowerSeries R}, IsUnit φ ↔ IsUnit (PowerSeries.constantCoeff φ)