mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.FiberBundle.Constructions
Bundle.Trivialization.Prod.left_inv : ∀ {B : Type u_1} [inst : TopologicalSpace B] {F₁ : Type u_2} [inst_1 : TopologicalSpace F₁] {E₁ : B → Type u_3}
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_4} [inst_3 : TopologicalSpace F₂]
  {E₂ : B → Type u_5} [inst_4 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  {e₁ : Bundle.Trivialization F₁ Bundle.TotalSpace.proj} {e₂ : Bundle.Trivialization F₂ Bundle.TotalSpace.proj}
  [inst_5 : (x : B) → Zero (E₁ x)] [inst_6 : (x : B) → Zero (E₂ x)]
  {x : Bundle.TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x},
  x ∈ Bundle.TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet) →
    Bundle.Trivialization.Prod.invFun' e₁ e₂ (Bundle.Trivialization.Prod.toFun' e₁ e₂ x) = x
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
/-- **Alias** of `CovariantDerivative.ContMDiffCovariantDerivative.affineCombination`.

---

An affine combination of two `C^k` connections is a `C^k` connection.  -/
CovariantDerivative.ContMDiffCovariantDerivative.affine_combination : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : ∀ (x : M), IsTopologicalAddGroup (V x)]
  [inst_13 : ∀ (x : M), ContinuousSMul 𝕜 (V x)] [inst_14 : FiberBundle F V] [inst_15 : IsManifold I 1 M]
  [inst_16 : VectorBundle 𝕜 F V] (cov cov' : CovariantDerivative I F V) {f : M → 𝕜} {n : WithTop ℕ∞},
  ContMDiff I (modelWithCornersSelf 𝕜 𝕜) n f →
    cov.ContMDiffCovariantDerivative n →
      cov'.ContMDiffCovariantDerivative n → (cov.affineCombination cov' f).ContMDiffCovariantDerivative n
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey?_insertManyIfNewUnit_empty_list_of_mem : ∀ {α : Type u} {instOrd : Ord α} [Std.TransOrd α] {l : List α} {k k' : α},
  compare k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬compare a b = Ordering.eq) l →
      k ∈ l →
        (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit Std.DTreeMap.Internal.Impl.empty l ⋯)).getKey? k' =
          some k
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
/-- The indexing type.  -/
CategoryTheory.Limits.FormalCoproduct.I : {C : Type u} → CategoryTheory.Limits.FormalCoproduct C → Type w
-- Mathlib.Order.Filter.AtTopBot.Tendsto
Filter.OrderBot.atBot_eq : ∀ (α : Type u_6) [inst : PartialOrder α] [inst_1 : OrderBot α], Filter.atBot = pure ⊥
-- Plausible.Testable
Plausible.Configuration.mk.inj : ∀ {numInst maxSize numRetries : ℕ} {traceDiscarded traceSuccesses traceShrink traceShrinkCandidates : Bool}
  {randomSeed : Option ℕ} {quiet sorryIfNoTestable : Bool} {numInst_1 maxSize_1 numRetries_1 : ℕ}
  {traceDiscarded_1 traceSuccesses_1 traceShrink_1 traceShrinkCandidates_1 : Bool} {randomSeed_1 : Option ℕ}
  {quiet_1 sorryIfNoTestable_1 : Bool},
  { numInst := numInst, maxSize := maxSize, numRetries := numRetries, traceDiscarded := traceDiscarded,
        traceSuccesses := traceSuccesses, traceShrink := traceShrink, traceShrinkCandidates := traceShrinkCandidates,
        randomSeed := randomSeed, quiet := quiet, sorryIfNoTestable := sorryIfNoTestable } =
      { numInst := numInst_1, maxSize := maxSize_1, numRetries := numRetries_1, traceDiscarded := traceDiscarded_1,
        traceSuccesses := traceSuccesses_1, traceShrink := traceShrink_1,
        traceShrinkCandidates := traceShrinkCandidates_1, randomSeed := randomSeed_1, quiet := quiet_1,
        sorryIfNoTestable := sorryIfNoTestable_1 } →
    numInst = numInst_1 ∧
      maxSize = maxSize_1 ∧
        numRetries = numRetries_1 ∧
          traceDiscarded = traceDiscarded_1 ∧
            traceSuccesses = traceSuccesses_1 ∧
              traceShrink = traceShrink_1 ∧
                traceShrinkCandidates = traceShrinkCandidates_1 ∧
                  randomSeed = randomSeed_1 ∧ quiet = quiet_1 ∧ sorryIfNoTestable = sorryIfNoTestable_1
-- Mathlib.Topology.Algebra.IntermediateField
IntermediateField.botContinuousSMul : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [inst_3 : TopologicalSpace L]
  [IsTopologicalRing L] (M : IntermediateField K L), ContinuousSMul ↥⊥ ↥M
-- Mathlib.Order.LiminfLimsup
Filter.blimsup_eq_limsup_subtype : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] {f : Filter β} {u : β → α} {p : β → Prop},
  Filter.blimsup u f p = Filter.limsup (u ∘ Subtype.val) (Filter.comap Subtype.val f)
-- Mathlib.Algebra.Homology.Refinements
HomologicalComplex.mono_homologyMap_iff_up_to_refinements : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} {K L : HomologicalComplex C c} (φ : K ⟶ L) (i j k : ι),
  c.prev j = i →
    c.next j = k →
      (CategoryTheory.Mono (HomologicalComplex.homologyMap φ j) ↔
        ∀ ⦃A : C⦄ (x₂ : A ⟶ K.X j),
          CategoryTheory.CategoryStruct.comp x₂ (K.d j k) = 0 →
            ∀ (y₁ : A ⟶ L.X i),
              CategoryTheory.CategoryStruct.comp x₂ (φ.f j) = CategoryTheory.CategoryStruct.comp y₁ (L.d i j) →
                ∃ A' π,
                  ∃ (_ : CategoryTheory.Epi π),
                    ∃ x₁, CategoryTheory.CategoryStruct.comp π x₂ = CategoryTheory.CategoryStruct.comp x₁ (K.d i j))
-- Mathlib.Order.Hom.CompleteLattice
CompleteLatticeHomClass.mk : ∀ {F : Type u_8} {α : Type u_9} {β : Type u_10} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  [inst_2 : FunLike F α β] [tosInfHomClass : sInfHomClass F α β] [tosSupHomClass : sSupHomClass F α β],
  CompleteLatticeHomClass F α β
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
/-- If `g` is a power series over a local ring such that
its image in the residue field is not zero, then `g` can be used as a Weierstrass divisor.  -/
PowerSeries.IsWeierstrassDivisor.of_map_ne_zero : ∀ {A : Type u_1} [inst : CommRing A] {g : PowerSeries A} [inst_1 : IsLocalRing A],
  (PowerSeries.map (IsLocalRing.residue A)) g ≠ 0 → g.IsWeierstrassDivisor
-- Mathlib.Util.DelabNonCanonical
/-- When the delab reader is pointed at an expression for an instance, returns `(true, t)`
iff instance synthesis succeeds and produces a defeq instance; otherwise returns `(false, t)`.
 -/
delabCheckingCanonical : Lean.PrettyPrinter.Delaborator.DelabM (Bool × Lean.Term)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get_erase : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α] (h : (↑m).WF) {k a : α} {h' : (m.erase k).contains a = true}, (m.erase k).get a h' = m.get a ⋯
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.content_eq_zero_iff : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : NormalizedGCDMonoid R] {p : Polynomial R}, p.content = 0 ↔ p = 0
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.encodeSigma.match_3.eq_1 : ∀ (motive : (n : ℕ) → (f : Fin n → ℕ) → (i : Fin n) × Fin (f i) → Sort u_1) (a : ℕ) (f : Fin (a + 1) → ℕ)
  (j : Fin (f 0)) (h_1 : (a : ℕ) → (f : Fin (a + 1) → ℕ) → (j : Fin (f 0)) → motive a.succ f ⟨⟨0, ⋯⟩, j⟩)
  (h_2 :
    (n : ℕ) →
      (f : Fin (n + 1) → ℕ) →
        (i : ℕ) → (hi : i + 1 < n + 1) → (j : Fin (f ⟨i + 1, hi⟩)) → motive n.succ f ⟨⟨i.succ, hi⟩, j⟩),
  (match a.succ, f, ⟨⟨0, ⋯⟩, j⟩ with
    | a.succ, f, ⟨⟨0, ⋯⟩, j⟩ => h_1 a f j
    | n.succ, f, ⟨⟨i.succ, hi⟩, j⟩ => h_2 n f i hi j) =
    h_1 a f j
-- Mathlib.ModelTheory.DirectLimit
/-- The direct limit `setoid` respects the structure `sigmaStructure`, so quotienting by it
gives rise to a valid structure.  -/
FirstOrder.Language.DirectLimit.prestructure : {L : FirstOrder.Language} →
  {ι : Type v} →
    [inst : Preorder ι] →
      (G : ι → Type w) →
        [inst_1 : (i : ι) → L.Structure (G i)] →
          (f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)) →
            [inst_2 : IsDirectedOrder ι] →
              [inst_3 : DirectedSystem G fun i j h => ⇑(f i j h)] →
                [Nonempty ι] → L.Prestructure (FirstOrder.Language.DirectLimit.setoid G f)
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.FiniteElement.val_add : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K]
  (x y : ArchimedeanClass.FiniteElement K), ↑(x + y) = ↑x + ↑y
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.sign_symm_trans_trans : ∀ {α : Type u} [inst : DecidableEq α] {β : Type v} [inst_1 : Fintype α] [inst_2 : DecidableEq β] [inst_3 : Fintype β]
  (f : Equiv.Perm α) (e : α ≃ β), Equiv.Perm.sign ((e.symm.trans f).trans e) = Equiv.Perm.sign f
-- Mathlib.Data.Matrix.Mul
/-- `v ᵥ* M` (notation for `vecMul v M`) is the vector-matrix product of vector `v` and matrix `M`,
where `v` is seen as a row vector.

The notation has precedence 73, which comes immediately before ` ⬝ᵥ ` for `dotProduct`,
so that `v ᵥ* A ⬝ᵥ w ᵥ* B` is parsed as `(v ᵥ* A) ⬝ᵥ (w ᵥ* B)`.
 -/
Matrix.vecMul : {m : Type u_2} →
  {n : Type u_3} → {α : Type v} → [NonUnitalNonAssocSemiring α] → [Fintype m] → (m → α) → Matrix m n α → n → α
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_rco_eq_if : ∀ {m n : ℤ}, (m...n).toArray = if m < n then #[m] ++ ((m + 1)...n).toArray else #[]
-- Mathlib.Data.Nat.Factorial.DoubleFactorial
Nat.doubleFactorial.eq_def : ∀ (x : ℕ),
  x.doubleFactorial =
    match x with
    | 0 => 1
    | 1 => 1
    | k.succ.succ => (k + 2) * k.doubleFactorial
-- Init.Data.UInt.Lemmas
UInt32.add_left_inj : ∀ {a b : UInt32} (c : UInt32), a + c = b + c ↔ a = b
-- Init.Data.Slice.Array.Basic
instSliceableArrayNatSubarray_5 : {α : Type u} → Std.Roi.Sliceable (Array α) ℕ (Subarray α)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- An iterated coproduct is a coproduct over a sigma type.  -/
CategoryTheory.Limits.sigmaSigmaIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {ι : Type u_1} →
      (f : ι → Type u_2) →
        (g : (i : ι) → f i → C) →
          [inst_1 : ∀ (i : ι), CategoryTheory.Limits.HasCoproduct (g i)] →
            [inst_2 : CategoryTheory.Limits.HasCoproduct fun i => ∐ g i] → (∐ fun i => ∐ g i) ≅ ∐ fun p => g p.fst p.snd
-- Mathlib.Lean.Json
Lean.instToJsonFin_mathlib : {n : ℕ} → Lean.ToJson (Fin n)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPolyC.go.match_4.congr_eq_4 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (x : Lean.Grind.CommRing.Expr)
  (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k))
  (h_2 : (k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k))
  (h_3 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k))
  (h_4 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_5 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_6 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b)) (h_7 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_8 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b))
  (h_9 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k)) (x_1 : Lean.Grind.CommRing.Var),
  x = Lean.Grind.CommRing.Expr.var x_1 →
    (match x with
      | Lean.Grind.CommRing.Expr.num k => h_1 k
      | Lean.Grind.CommRing.Expr.natCast k => h_2 k
      | Lean.Grind.CommRing.Expr.intCast k => h_3 k
      | Lean.Grind.CommRing.Expr.var x => h_4 x
      | a.add b => h_5 a b
      | a.mul b => h_6 a b
      | a.neg => h_7 a
      | a.sub b => h_8 a b
      | a.pow k => h_9 a k) ≍
      h_4 x_1
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Functor.reflectsMonomorphisms_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [F.ReflectsMonomorphisms] [G.ReflectsMonomorphisms], (F.comp G).ReflectsMonomorphisms
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.one_mono : ∀ {α : Type u_5} {β : Type u_6} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : One β], Monotone 1
-- Lean.Meta.Tactic.Grind.Types
/-- Returns `true` if `a` and `b` are in the same equivalence class.  -/
Lean.Meta.Grind.isEqv : Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Bool
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.arrowCongr.congr_simp : ∀ {R₁ : Type u_9} {R₂ : Type u_10} {R₁' : Type u_12} {R₂' : Type u_13} {M₁ : Type u_17} {M₂ : Type u_18}
  {M₁' : Type u_20} {M₂' : Type u_21} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : CommSemiring R₁']
  [inst_3 : CommSemiring R₂'] [inst_4 : AddCommMonoid M₁] [inst_5 : AddCommMonoid M₂] [inst_6 : AddCommMonoid M₁']
  [inst_7 : AddCommMonoid M₂'] [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] [inst_10 : Module R₁' M₁']
  [inst_11 : Module R₂' M₂'] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₁'₂' : R₁' →+* R₂'} {σ₂'₁' : R₂' →+* R₁'}
  {σ₁₁' : R₁ →+* R₁'} {σ₂₂' : R₂ →+* R₂'} {σ₂₁' σ₂₁'_1 : R₂ →+* R₁'} (e_σ₂₁' : σ₂₁' = σ₂₁'_1) {σ₁₂' σ₁₂'_1 : R₁ →+* R₂'}
  (e_σ₁₂' : σ₁₂' = σ₁₂'_1) [inst_12 : RingHomInvPair σ₁₂ σ₂₁] [inst_13 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_14 : RingHomInvPair σ₁'₂' σ₂'₁'] [inst_15 : RingHomInvPair σ₂'₁' σ₁'₂']
  [inst_16 : RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'] [inst_17 : RingHomCompTriple σ₂₁ σ₁₂' σ₂₂']
  [inst_18 : RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'] [inst_19 : RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'] (e₁ e₁_1 : M₁ ≃ₛₗ[σ₁₂] M₂),
  e₁ = e₁_1 → ∀ (e₂ e₂_1 : M₁' ≃ₛₗ[σ₁'₂'] M₂'), e₂ = e₂_1 → e₁.arrowCongr e₂ = e₁_1.arrowCongr e₂_1
-- Mathlib.RingTheory.Derivation.Basic
Derivation.coe_comp : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M] (D : Derivation R A M)
  {N : Type u_5} [inst_6 : AddCommMonoid N] [inst_7 : Module A N] [inst_8 : Module R N] [inst_9 : IsScalarTower R A M]
  [inst_10 : IsScalarTower R A N] (f : M →ₗ[A] N), ⇑(f.compDer D) = ⇑(↑R f ∘ₗ ↑D)
-- Mathlib.Geometry.Manifold.Instances.Real
/-- A product `M × [x,y]` for `M` boundaryless has boundary `M × {x, y}`.  -/
boundary_product : ∀ {x y : ℝ} [hxy : Fact (x < y)] {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2}
  [inst_2 : TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] [I.Boundaryless], ModelWithCorners.boundary (M × ↑(Set.Icc x y)) = Set.univ.prod {⊥, ⊤}
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- A bicone over `P Q : C`, which is both a limit cone and a colimit cocone.  -/
CategoryTheory.Limits.BinaryBiproductData.bicone : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {P Q : C} → CategoryTheory.Limits.BinaryBiproductData P Q → CategoryTheory.Limits.BinaryBicone P Q
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.rootSpan_dualAnnihilator_map_eq : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N),
  Submodule.map (↑P.flip.toPerfPair.symm) (P.rootSpan R).dualAnnihilator =
    (Submodule.span R (Set.range P.root')).dualCoannihilator
-- Mathlib.RingTheory.Perfection
PreTilt.instCommRing : (O : Type u₂) → [inst : CommRing O] → (p : ℕ) → [Fact (Nat.Prime p)] → [Fact ¬IsUnit ↑p] → CommRing (PreTilt O p)
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.congr_symm : ∀ {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M]
  [inst_6 : IsScalarTower R A M] [inst_7 : AddCommMonoid N] [inst_8 : Module R N] [inst_9 : AddCommMonoid P]
  [inst_10 : Module R P] [inst_11 : Module A P] [inst_12 : IsScalarTower R A P] [inst_13 : AddCommMonoid Q]
  [inst_14 : Module R Q] (f : M ≃ₗ[A] P) (g : N ≃ₗ[R] Q),
  TensorProduct.AlgebraTensorModule.congr f.symm g.symm = (TensorProduct.AlgebraTensorModule.congr f g).symm
-- Mathlib.Analysis.Normed.Module.WeakDual
WeakDual.extendRCLikeL_apply_apply : ∀ {𝕜 : Type u_5} {F : Type u_7} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [inst_3 : TopologicalSpace F] [inst_4 : ContinuousConstSMul 𝕜 F] [inst_5 : Module ℝ F] [inst_6 : IsScalarTower ℝ 𝕜 F]
  (f : WeakDual ℝ F) (x : F), (WeakDual.extendRCLikeL f) x = ↑(f x) - RCLike.I • ↑(f (RCLike.I • x))
-- Mathlib.Algebra.Ring.Action.Rat
NNRat.instDistribSMul : {R : Type u_1} → [inst : DivisionSemiring R] → DistribSMul ℚ≥0 R
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Polynomial.IsDistinguishedAt.isWeierstrassDivisorAt : ∀ {A : Type u_1} [inst : CommRing A] {g : Polynomial A} {I : Ideal A},
  g.IsDistinguishedAt I → I ≠ ⊤ → (↑g).IsWeierstrassDivisorAt I
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
_private.Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory.0.CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.unitIso_hom_app_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] (X : CategoryTheory.Comon (CategoryTheory.Functor C D)) (x : C),
  (CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.unitIso✝.hom.app X).hom.app x =
    CategoryTheory.CategoryStruct.id (X.X.obj x)
-- Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric
_private.Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric.0.Complex.multiset_prod_eq_pow_mul_multiset_prod : ∀ {n : ℕ} (a : Multiset ℂ),
  n ≠ 0 → (Multiset.map (fun x => x + ↑n) a).prod = ↑n ^ a.card * (Multiset.map (fun x => x / ↑n + 1) a).prod
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
linearIndepOn_finset_iffₛ : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] {s : Finset ι},
  LinearIndepOn R v ↑s ↔ ∀ (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleConfig.buildLocalRule : Aesop.Frontend.RuleConfig → Aesop.ElabM Aesop.LocalRuleSetMember
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
lt_of_lt_mul_of_le_one_left : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulLeftMono α] {a b c : α}, a < b * c → c ≤ 1 → a < b
-- ProofWidgets.Component.RefreshComponent
ProofWidgets.RefreshComponent.instRpcEncodableProps : Lean.Server.RpcEncodable ProofWidgets.RefreshComponent.Props
-- Mathlib.Topology.Maps.Strict.Group
/-- A group homomorphism is strict if and only if its `QuotientGroup.kerLift` is an embedding.  -/
MonoidHom.isStrictMap_iff_isEmbedding_kerLift : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] {f : G →* H} [inst_2 : TopologicalSpace G]
  [inst_3 : TopologicalSpace H], Topology.IsStrictMap ⇑f ↔ Topology.IsEmbedding ⇑(QuotientGroup.kerLift f)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentSymbolAux.mk : {Self : Type} →
  String →
    Option String →
      Lean.Lsp.SymbolKind → Lean.Lsp.Range → Lean.Lsp.Range → Option (Array Self) → Lean.Lsp.DocumentSymbolAux Self
-- Mathlib.CategoryTheory.ObjectProperty.Basic
CategoryTheory.ObjectProperty.is_of_prop : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] (P : CategoryTheory.ObjectProperty C) {X : C},
  P X → P.Is X
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.hasSum_coe : ∀ {α : Type u_1} {f : α → NNReal} {r : NNReal}, HasSum (fun a => ↑(f a)) ↑r ↔ HasSum f r
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.isAddMonHom_ofIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M X : C}
  [inst_2 : CategoryTheory.AddMonObj M] (e : M ≅ X), CategoryTheory.IsAddMonHom e.hom
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instMulActionAddMonoidHomOfDistribMulAction : {A : Type u_5} →
  {M : Type u_6} →
    {B : Type u_7} →
      [inst : Monoid M] →
        [inst_1 : AddMonoid A] → [DistribMulAction M A] → [inst_3 : AddZeroClass B] → MulAction Mᵈᵐᵃ (A →+ B)
-- Mathlib.Analysis.Normed.Field.Basic
NormedField.toMetricSpace : {α : Type u_5} → [self : NormedField α] → MetricSpace α
-- Mathlib.Algebra.Homology.ComplexShape
/-- The `ComplexShape` appropriate for cohomology, so `d : X i ⟶ X j` only when `j = i + 1`.
 -/
ComplexShape.up : (α : Type u_2) → [inst : Add α] → [IsRightCancelAdd α] → [One α] → ComplexShape α
-- Mathlib.Algebra.Group.Submonoid.Support
AddSubmonoid.IsSpanning.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] (M : AddSubmonoid G), M.IsSpanning = ∀ (a : G), a ∈ M ∨ -a ∈ M
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey!_eq_getLast!_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t.maxKey! = t.keys.getLast!
-- Mathlib.Order.RelClasses
/-- Set notation form of `LE.le.trans_lt` -/
LE.le.trans_ssubset : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : Preorder α] {a b c : α}, a ⊆ b → b ⊂ c → a ⊂ c
-- Mathlib.Logic.Relator
Relator.LeftTotal.symm : ∀ {α : Type u_1} {β : Type u_2} {r₁₂ : α → β → Prop} {r₂₁ : β → α → Prop},
  (∀ (a : α) (b : β), r₁₂ a b → r₂₁ b a) → Relator.LeftTotal r₁₂ → Relator.RightTotal r₂₁
-- Init.Data.Slice.List.Lemmas
ListSlice.toList_mkSlice_roi : ∀ {α : Type u_1} {xs : ListSlice α} {lo : ℕ},
  Std.Slice.toList (Std.Roi.Sliceable.mkSlice xs lo<...*) = List.drop (lo + 1) (Std.Slice.toList xs)
-- Mathlib.Algebra.BigOperators.Group.List.Basic
/-- We'd like to state this as `L.headI * L.tail.prod = L.prod`, but because `L.headI` relies on an
inhabited instance to return a garbage value on the empty list, this is not possible.
Instead, we write the statement in terms of `L[0]?.getD 1`.
 -/
List.getElem?_zero_mul_tail_prod : ∀ {M : Type u_4} [inst : Monoid M] (l : List M), l[0]?.getD 1 * l.tail.prod = l.prod
-- Aesop.Forward.LevelIndex
Aesop.instLELevelIndex : LE Aesop.LevelIndex
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- Multiplying the products of a function over `s` and over `sᶜ` gives the whole product.
For a version expressed with subtypes, see `Fintype.prod_subtype_mul_prod_subtype`.  -/
Finset.prod_mul_prod_compl : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (s : Finset ι)
  (f : ι → M), (∏ i ∈ s, f i) * ∏ i ∈ sᶜ, f i = ∏ i, f i
-- Mathlib.CategoryTheory.GradedObject.Monoidal
/-- Auxiliary definition for `associator`.  -/
CategoryTheory.GradedObject.Monoidal.triangleIndexData : (I : Type u) →
  [inst : AddMonoid I] →
    CategoryTheory.GradedObject.TriangleIndexData CategoryTheory.GradedObject.Monoidal.r₁₂₃ fun x =>
      match x with
      | (i₁, i₃) => i₁ + i₃
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.Equivalence.prod_counitIso : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D] (E₁ : A ≌ B) (E₂ : C ≌ D),
  (E₁.prod E₂).counitIso = CategoryTheory.NatIso.prod E₁.counitIso E₂.counitIso
-- Mathlib.Combinatorics.Colex
Finset.Colex.instLE : {α : Type u_1} → [PartialOrder α] → LE (Colex (Finset α))
-- Mathlib.Topology.MetricSpace.Holder
HolderWith.mono : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {C r : NNReal} {f : X → Y}
  {C' : NNReal}, HolderWith C r f → C ≤ C' → HolderWith C' r f
-- Mathlib.Data.Int.Fib.Basic
Int.fib_one : Int.fib 1 = 1