mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.Linarith.Verification
/-- Inner loop for `addExprs'`.  -/
_private.Mathlib.Tactic.Linarith.Verification.0.Mathlib.Tactic.Linarith.addExprs'.go : {u : Lean.Level} →
  {α :
      have u := u;
      Q(Type u)} →
    Q(AddMonoid «$α») → Q(«$α») → List Q(«$α») → Q(«$α»)
-- Mathlib.SetTheory.Cardinal.Ordinal
Ordinal.card_iSup_Iio_le_sum_card : ∀ {o : Ordinal.{u}} (f : ↑(Set.Iio o) → Ordinal.{max u v}), (⨆ a, f a).card ≤ Cardinal.sum fun i => (f i.toOrd).card
-- Init.Grind.AC
Lean.Grind.AC.Seq.denote_insert_of_contains : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) [inst₁ : Std.Associative ctx.op] [inst₂ : Std.Commutative ctx.op]
  [inst₃ : Std.IdempotentOp ctx.op] (s : Lean.Grind.AC.Seq) (x : Lean.Grind.AC.Var),
  s.contains_k x = true → Lean.Grind.AC.Seq.denote ctx (Lean.Grind.AC.Seq.insert x s) = Lean.Grind.AC.Seq.denote ctx s
-- Mathlib.Topology.Algebra.Group.Basic
IsTopologicalAddGroup.isInducing_iff_nhds_zero : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] {H : Type u_1}
  [inst_3 : AddGroup H] [inst_4 : TopologicalSpace H] [IsTopologicalAddGroup H] {F : Type u_2} [inst_6 : FunLike F G H]
  [AddMonoidHomClass F G H] {f : F}, Topology.IsInducing ⇑f ↔ nhds 0 = Filter.comap (⇑f) (nhds 0)
-- Mathlib.Geometry.Manifold.Submersion
/-- If `f` is a submersion at `x`, it maps its domain chart's target to its codomain chart's target:
`(h.domChart.extend I).target` to `(h.domChart.extend J).target`.

See `target_subset_preimage_target` for a version stated using preimages instead of images.
 -/
Manifold.IsSubmersionAtOfComplement.image_target_subset_target : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {F : Type u_5} {H : Type u_7} {G : Type u_9} {E : Type u}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace 𝕜 F] [inst_7 : TopologicalSpace H] [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [inst_9 : TopologicalSpace M]
  [inst_10 : ChartedSpace H M] [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N}
  {x : M} (h : Manifold.IsSubmersionAtOfComplement F I J n f x),
  Prod.fst ∘ ⇑h.equiv '' (h.domChart.extend I).target ⊆ (h.codChart.extend J).target
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardSliceSearcher.le_of_matchesAt : ∀ {pat s : String.Slice} {pos : s.Pos},
  pat.isEmpty = false →
    String.Slice.Pattern.Model.MatchesAt pat pos → pos.offset.increaseBy pat.utf8ByteSize ≤ s.rawEndPos
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
/-- A formal coproduct is an indexed set of objects, where ⟨I, f⟩ corresponds to the "formal
coproduct" `⨿ (i : I), f i`, where `f i : C` is the `i`ᵗʰ component.  -/
CategoryTheory.Limits.FormalCoproduct : Type u → Type (max u (w + 1))
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctor.mk'_mapComp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (S : CategoryTheory.StrictPseudofunctorCore B C) {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  (CategoryTheory.StrictPseudofunctor.mk' S).mapComp f g = CategoryTheory.eqToIso ⋯
-- Init.Tactics
/-- `mright` is like `right`, but operating on a stateful `Std.Do.SPred` goal.
```lean
example (P Q : SPred σs) : P ⊢ₛ Q ∨ P := by
  mintro HP
  mright
  mexact HP
```
 -/
Lean.Parser.Tactic.mrightMacro : Lean.ParserDescr
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instOrderTop : {α : Type u_1} → {β : Type u_2} → {l : Filter α} → [inst : LE β] → [OrderTop β] → OrderTop (l.Germ β)
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.nontrivial_of_diam_ne_zero : ∀ {α : Type u_1} {G : SimpleGraph α}, G.diam ≠ 0 → Nontrivial α
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.Functor.homRel_iff : ∀ {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] (F : CategoryTheory.Functor C D) {X Y : C} (f g : X ⟶ Y),
  F.homRel f g ↔ F.map f = F.map g
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite
CategoryTheory.Limits.CreatesColimitsOfSize0.createsFiniteColimits : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [CategoryTheory.CreatesColimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F] →
            CategoryTheory.Limits.CreatesFiniteColimits F
-- Mathlib.MeasureTheory.Function.LpSpace.Indicator
MeasureTheory.indicatorConstLp_coeFn : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {s : Set α} {hs : MeasurableSet s} {hμs : μ s ≠ ⊤} {c : E},
  ↑↑(MeasureTheory.indicatorConstLp p hs hμs c) =ᵐ[μ] s.indicator fun x => c
-- Mathlib.Algebra.Group.Pi.Units
AddEquiv.val_neg_piAddUnits_apply : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → AddMonoid (M i)] (f : AddUnits ((i : ι) → M i)) (i : ι),
  ↑(-AddEquiv.piAddUnits f i) = f.neg i
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_inter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (t₁ ∩ t₂).getKey? k = if k ∈ t₂ then t₁.getKey? k else none
-- Mathlib.Data.Vector3
Fin2.add.eq_2 : ∀ {n : ℕ} (i : Fin2 n) (k : ℕ), i.add k.succ = (i.add k).fs
-- Mathlib.Analysis.InnerProductSpace.Basic
parallelogram_law_with_norm_mul : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E),
  ‖x + y‖ * ‖x + y‖ + ‖x - y‖ * ‖x - y‖ = 2 * (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)
-- Mathlib.Algebra.Lie.Nilpotent
LieIdeal.map_lowerCentralSeries_le : ∀ {R : Type u} {L : Type v} {L' : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing L'] [inst_4 : LieAlgebra R L'] (k : ℕ) {f : L →ₗ⁅R⁆ L'},
  LieIdeal.map f (LieModule.lowerCentralSeries R L L k) ≤ LieModule.lowerCentralSeries R L' L' k
-- Lean.DocString.Syntax
/-- Verso inline objects. These are part of the ordinary text flow of a paragraph.

This syntax uses the following conventions:
* Sequences of inline items are in square brackets
* Literal data, like strings or numbers, are in parentheses
* Verso metaprogram names and arguments are in curly braces
 -/
Lean.Parser.Category.inline : Lean.Parser.Category
-- Mathlib.Algebra.Order.Group.Action.Synonym
Lex.instMulAction'.eq_1 : ∀ {M : Type u_1} {α : Type u_3} [inst : Monoid M] [inst_1 : MulAction M α],
  Lex.instMulAction' = { toSMul := Lex.instSMul, mul_smul := ⋯, one_smul := ⋯ }
-- Mathlib.Order.Interval.Set.Monotone
Monotone.Iio : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Monotone f → Monotone fun x => Set.Iio (f x)
-- Mathlib.Topology.UniformSpace.Cauchy
Cauchy.mono : ∀ {α : Type u} [uniformSpace : UniformSpace α] {f g : Filter α} [hg : g.NeBot], Cauchy f → g ≤ f → Cauchy g
-- Std.Data.ExtDTreeMap.Basic
/-- Retrieves the key from the mapping that matches `a`. Ensures that such a mapping exists by
requiring a proof of `a ∈ m`. The result is guaranteed to be pointer equal to the key in the map.
 -/
Std.ExtDTreeMap.getKey : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → [inst : Std.TransCmp cmp] → (t : Std.ExtDTreeMap α β cmp) → (a : α) → a ∈ t → α
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_castLEEmb_Icc : ∀ {n m : ℕ} (a b : Fin n) (h : n ≤ m),
  Finset.map (Fin.castLEEmb h) (Finset.Icc a b) = Finset.Icc (Fin.castLE h a) (Fin.castLE h b)
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MRefinePat.pure.inj : ∀ {h h_1 : Lean.TSyntax `term}, Lean.Parser.Tactic.MRefinePat.pure h = Lean.Parser.Tactic.MRefinePat.pure h_1 → h = h_1
-- Std.Data.DTreeMap.Internal.Lemmas
_private.Std.Data.DTreeMap.Internal.Lemmas.0.Std.DTreeMap.Internal.Impl.cast_eq_id : ∀ {α : Type u}, cast ⋯ = id
-- Mathlib.Algebra.Central.TensorProduct
Algebra.IsCentral.right_of_tensor : ∀ (K : Type u_1) (B : Type u_2) (C : Type u_3) [inst : CommSemiring K] [inst_1 : Semiring B] [inst_2 : Semiring C]
  [inst_3 : Algebra K B] [inst_4 : Algebra K C],
  Function.Injective ⇑(algebraMap K B) →
    ∀ [Module.Flat K C] [Algebra.IsCentral K (TensorProduct K B C)], Algebra.IsCentral K C
-- Mathlib.Data.Set.Lattice
Set.iUnion_mono'' : ∀ {α : Type u_1} {ι : Sort u_5} {s t : ι → Set α}, (∀ (i : ι), s i ⊆ t i) → Set.iUnion s ⊆ Set.iUnion t
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.anyM_toList : ∀ {α β : Type w} {m : Type → Type w'} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α Id m] [Std.LawfulIteratorLoop α Id m] {it : Std.Iter β} {p : β → m Bool},
  List.anyM p it.toList = Std.Iter.anyM p it
-- Mathlib.Data.Finset.NatAntidiagonal
Finset.Nat.antidiagonal_succ : ∀ (n : ℕ),
  Finset.HasAntidiagonal.antidiagonal (n + 1) =
    Finset.cons (0, n + 1)
      (Finset.map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Function.Embedding.refl ℕ))
        (Finset.HasAntidiagonal.antidiagonal n))
      ⋯
-- Mathlib.Dynamics.Ergodic.Ergodic
Ergodic.ae_empty_or_univ_of_ae_le_preimage : ∀ {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {f : α → α} {μ : MeasureTheory.Measure α}
  [MeasureTheory.IsFiniteMeasure μ],
  Ergodic f μ → MeasureTheory.NullMeasurableSet s μ → s ≤ᵐ[μ] f ⁻¹' s → s =ᵐ[μ] ∅ ∨ s =ᵐ[μ] Set.univ
-- Mathlib.Order.BoundedOrder.Basic
Pi.bot_comp : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : Bot γ] (x : α → β), ⊥ ∘ x = ⊥
-- Mathlib.Geometry.Euclidean.SignedDist
signedDist_eq_zero_of_orthogonal : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {v : V} {p q : P}, inner ℝ v (q -ᵥ p) = 0 → ((signedDist v) p) q = 0
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.isValidLe.eq_1 : ∀ (k : ℤ), (Int.Internal.Linear.Poly.num k).isValidLe = decide (k ≤ 0)
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
_private.Mathlib.CategoryTheory.Bicategory.InducedBicategory.0.CategoryTheory.Bicategory.InducedBicategory.Hom.mk : {B : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Bicategory C] →
      {F : B → C} → {X Y : CategoryTheory.Bicategory.InducedBicategory C F} → (F X ⟶ F Y) → X.Hom Y
-- Mathlib.Data.Finset.Card
Finset.subset_iff_eq_of_card_le : ∀ {α : Type u_1} {s t : Finset α}, t.card ≤ s.card → (s ⊆ t ↔ s = t)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
/-- The type of functors out of the chosen terminal category is equivalent to the type of objects
in the target category. TODO: upgrade to an equivalence of categories.  -/
CategoryTheory.Cat.fromChosenTerminalEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor (↑CategoryTheory.Cat.chosenTerminal) C ≃ C
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.LaxTrans.Hom.ext_iff : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} {x y : CategoryTheory.Oplax.LaxTrans.Hom η θ},
  x = y ↔ x.as = y.as
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get?_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k a : α}, (t.insert k).get? a = if cmp k a = Ordering.eq ∧ k ∉ t then some k else t.get? a
-- Mathlib.Topology.UniformSpace.AbstractCompletion
AbstractCompletion.induction_on : ∀ {α : Type uα} [inst : UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {p : pkg.space → Prop} (a : pkg.space),
  IsClosed {a | p a} → (∀ (a : α), p (pkg.coe a)) → p a
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.id.eq_1 : ∀ (M : Type u_2) {X : Type u_5} [inst : SMul M X], MulActionHom.id M = { toFun := fun x => x, map_smul' := ⋯ }
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
pos_of_lt_add_left : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LT α] [AddRightReflectLT α] {a b : α}, b < a + b → 0 < a
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.isTheta_smoothingFn_sub_self : ∀ {α : Type u_1} [inst : Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [inst_1 : Nonempty α]
  (R : AkraBazziRecurrence T g a b r) (i : α),
  (fun n => AkraBazziRecurrence.smoothingFn (b i * ↑n) - AkraBazziRecurrence.smoothingFn ↑n) =Θ[Filter.atTop] fun n =>
    1 / Real.log ↑n ^ 2
-- Mathlib.Algebra.Group.Subgroup.Basic
AddMonoidHom.ker_snd : ∀ {G : Type u_1} {G' : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup G'], (AddMonoidHom.snd G G').ker = ⊤.prod ⊥
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
CategoryTheory.ProjectiveResolution.lift.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {Y Z : C} (f : Y ⟶ Z)
  (P : CategoryTheory.ProjectiveResolution Y) (Q : CategoryTheory.ProjectiveResolution Z),
  CategoryTheory.ProjectiveResolution.lift f P Q =
    P.complex.mkHom Q.complex (CategoryTheory.ProjectiveResolution.liftFZero f P Q)
      (CategoryTheory.ProjectiveResolution.liftFOne f P Q) ⋯ fun n x =>
      match x with
      | ⟨g, ⟨g', w⟩⟩ => ⟨(P.liftFSucc Q n g g' w).fst, ⋯⟩
-- Mathlib.CategoryTheory.Monad.Products
CategoryTheory.underToAlgebra_obj_a : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C]
  (f : CategoryTheory.Under X),
  ((CategoryTheory.underToAlgebra X).obj f).a =
    CategoryTheory.Limits.coprod.desc f.hom (CategoryTheory.CategoryStruct.id f.right)
-- Mathlib.Algebra.Category.Ring.FinitePresentation
/-- If `S` is a finitely presented `R`-algebra, then `Hom_R(S, -)` preserves filtered colimits.  -/
CommRingCat.preservesFilteredColimits_coyoneda : ∀ (R : CommRingCat) (S : CategoryTheory.Under R),
  (CommRingCat.Hom.hom S.hom).FinitePresentation →
    CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.coyoneda.obj (Opposite.op S))
-- Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsFunctorPreservesColimitsOfShape : ∀ {J : Type u_1} {C : Type u_3} (K : Type u_5) [inst : CategoryTheory.Category.{v_1, u_5} K]
  [inst_1 : CategoryTheory.Category.{v_3, u_1} J] [inst_2 : CategoryTheory.Category.{v_5, u_3} C],
  (CategoryTheory.ObjectProperty.preservesColimitsOfShape K).IsClosedUnderIsomorphisms
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
/-- The largest variable index that has not been (officially) eliminated.  -/
Mathlib.Tactic.Linarith.LinarithData.maxVar : Mathlib.Tactic.Linarith.LinarithData → ℕ
-- Mathlib.Order.Category.BddOrd
BddOrd.ofHom_apply : ∀ {X Y : Type u} [inst : PartialOrder X] [inst_1 : BoundedOrder X] [inst_2 : PartialOrder Y] [inst_3 : BoundedOrder Y]
  (f : BoundedOrderHom X Y) (x : X), (CategoryTheory.ConcreteCategory.hom (BddOrd.ofHom f)) x = f x
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
CategoryTheory.Localization.SmallShiftedHom.shift.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {W : CategoryTheory.MorphismProperty C} {M : Type w'}
  [inst_1 : AddMonoid M] [inst_2 : CategoryTheory.HasShift C M] [inst_3 : W.IsCompatibleWithShift M] {X Y : C} {a : M}
  [inst_4 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y]
  [inst_5 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y Y]
  (f f_1 : CategoryTheory.Localization.SmallShiftedHom W X Y a),
  f = f_1 → ∀ (n a' : M) (h : a + n = a'), f.shift n a' h = f_1.shift n a' h
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
/-- **Alias** of `MeasureTheory.lintegral_finsetSum_measure`. -/
MeasureTheory.lintegral_finset_sum_measure : ∀ {α : Type u_1} {m : MeasurableSpace α} {ι : Type u_4} (s : Finset ι) (f : α → ENNReal)
  (μ : ι → MeasureTheory.Measure α), ∫⁻ (a : α), f a ∂∑ i ∈ s, μ i = ∑ i ∈ s, ∫⁻ (a : α), f a ∂μ i
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.get!_eq_get!ₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] [inst_2 : Hashable α]
  (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) [inst_3 : Inhabited (β a)], m.get! a = m.get!ₘ a
-- Init.Data.SInt.Bitwise
Int32.xor_neg_one : ∀ {a : Int32}, a ^^^ -1 = ~~~a
-- Mathlib.LinearAlgebra.TensorProduct.Tower
/-- Heterobasic version of `LinearMap.lTensor`  -/
TensorProduct.AlgebraTensorModule.lTensor : {R : Type uR} →
  (A : Type uA) →
    (M : Type uM) →
      {N : Type uN} →
        {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 Q] →
                              [inst_10 : Module R Q] → (N →ₗ[R] Q) →ₗ[R] TensorProduct R M N →ₗ[A] TensorProduct R M Q
-- Mathlib.Topology.EMetricSpace.Weak
/-- The one point compactification of a weak pseudo extended metric space is again a weak pseudo
extended metric space.  -/
instWeakPseudoEMetricSpaceOnePoint : {α : Type u} → [t : TopologicalSpace α] → [m : WeakPseudoEMetricSpace α] → WeakPseudoEMetricSpace (OnePoint α)
-- Mathlib.Analysis.Calculus.ImplicitContDiff
/-- `implicitFunction` is indeed the (local) implicit function defined by `f`.  -/
ContDiffAt.eventually_apply_implicitFunction : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E₁ : Type u_2} [inst_1 : NormedAddCommGroup E₁] [inst_2 : NormedSpace 𝕜 E₁]
  [inst_3 : CompleteSpace E₁] {E₂ : Type u_3} [inst_4 : NormedAddCommGroup E₂] [inst_5 : NormedSpace 𝕜 E₂]
  [inst_6 : CompleteSpace E₂] {F : Type u_4} [inst_7 : NormedAddCommGroup F] [inst_8 : NormedSpace 𝕜 F]
  [inst_9 : CompleteSpace F] {u : E₁ × E₂} {f : E₁ × E₂ → F} {n : WithTop ℕ∞} (cdf : ContDiffAt 𝕜 n f u) (pn : n ≠ 0)
  (if₂ : (fderiv 𝕜 f u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible),
  ∀ᶠ (x : E₁) in nhds u.1, f (x, cdf.implicitFunction pn if₂ x) = f u
-- Mathlib.LinearAlgebra.Projection
/-- **Alias** of `Submodule.projectionOnto_apply_left`. -/
Submodule.linearProjOfIsCompl_apply_left : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (h : IsCompl p q) (x : ↥p), (p.projectionOnto q h) ↑x = x
-- Mathlib.Algebra.Group.Defs
SubNegMonoid.toNeg : {G : Type u} → [self : SubNegMonoid G] → Neg G
-- Mathlib.Analysis.Analytic.Within
AnalyticWithinAt.exists_mem_nhdsWithin_analyticOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F}
  {s : Set E} {x : E}, AnalyticWithinAt 𝕜 f s x → ∃ u ∈ nhdsWithin x (insert x s), AnalyticOn 𝕜 f u
-- Std.Data.DTreeMap.Raw.Slice
Std.DTreeMap.Raw.toList_rci : ∀ {α : Type u} {β : α → Type v} (cmp : autoParam (α → α → Ordering) Std.DTreeMap.Raw.toList_rci._auto_1)
  [Std.TransCmp cmp] {t : Std.DTreeMap.Raw α β cmp},
  t.WF →
    ∀ {bound : α},
      Std.Slice.toList (Std.Rci.Sliceable.mkSlice t bound...*) = List.filter (fun e => (cmp e.fst bound).isGE) t.toList
-- Mathlib.CategoryTheory.Limits.Preorder
Preorder.coconeOfUpperBound_pt : ∀ {C : Type u} [inst : Preorder C] {J : Type u'} [inst_1 : CategoryTheory.Category.{v, u'} J]
  (F : CategoryTheory.Functor J C) {x : C} (h : x ∈ upperBounds (Set.range F.obj)),
  (Preorder.coconeOfUpperBound F h).pt = x
-- Mathlib.Topology.Sheaves.Flasque
/-- A sheaf is flasque if all of the restriction morphisms are epimorphisms.  -/
TopCat.Presheaf.IsFlasque : {X : TopCat} → {C : Type v} → [inst : CategoryTheory.Category.{w, v} C] → TopCat.Presheaf C X → Prop
-- Mathlib.Tactic.Positivity.Basic
/-- The `positivity` extension which identifies expressions of the form `a - b`,
such that there is a local hypothesis `b < a`, `b ≤ a`, `a ≠ b` or `b ≠ a`.  -/
Mathlib.Meta.Positivity.evalSub : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Data.ENNReal.Inv
ENNReal.lt_inv_iff_lt_inv : ∀ {a b : ENNReal}, a < b⁻¹ ↔ b < a⁻¹
-- Mathlib.Algebra.Prime.Defs
not_prime_one : ∀ {M : Type u_1} [inst : CommMonoidWithZero M], ¬Prime 1
-- Aesop.Search.Queue
Aesop.FIFOQueue.addGoals : Aesop.FIFOQueue → Array Aesop.GoalRef → Aesop.FIFOQueue
-- Lean.Parser.Syntax
Lean.Parser.Command.macroArg.formatter : Lean.PrettyPrinter.Formatter
-- Lean.Meta.Tactic.Grind.AC.PP
_private.Lean.Meta.Tactic.Grind.AC.PP.0.Lean.Meta.Grind.AC.M : Type → Type
-- Mathlib.Data.Part
Part.some_dom : ∀ {α : Type u_1} (a : α), (Part.some a).Dom
-- Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily
ProbabilityTheory.BrownianReal.covariance_eval_projectiveFamily : ∀ (I : Finset NNReal) (s t : ↥I),
  ProbabilityTheory.covariance (fun x => x s) (fun x => x t) (ProbabilityTheory.BrownianReal.projectiveFamily I) =
    ↑(min ↑s ↑t)
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
/-- `cyclotomic n R` comes from `cyclotomic n ℤ`.  -/
Polynomial.map_cyclotomic_int : ∀ (n : ℕ) (R : Type u_1) [inst : Ring R],
  Polynomial.map (Int.castRingHom R) (Polynomial.cyclotomic n ℤ) = Polynomial.cyclotomic n R
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.GLPos.coe_neg : ∀ {n : Type u} {R : Type v} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing R] [inst_3 : LinearOrder R]
  [inst_4 : IsStrictOrderedRing R] [inst_5 : Fact (Even (Fintype.card n))] (g : ↥(Matrix.GLPos n R)), ↑↑(-g) = -↑↑g
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric
CFC.continuousOn_sqrt : ∀ {A : Type u_1} [inst : NonUnitalNormedRing A] [inst_1 : StarRing A] [inst_2 : NormedSpace ℝ A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : SMulCommClass ℝ A A] [inst_5 : PartialOrder A] [inst_6 : StarOrderedRing A]
  [inst_7 : NonnegSpectrumClass ℝ A] [inst_8 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [ContinuousStar A] [CompleteSpace A], ContinuousOn CFC.sqrt {a | 0 ≤ a}
-- Mathlib.Topology.Spectral.Hom
SpectralMap.coe_copy : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : SpectralMap α β)
  (f' : α → β) (h : f' = ⇑f), ⇑(f.copy f' h) = f'
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.monoidalPi_μ : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] {D : I → Type u₂}
  [inst_2 : (i : I) → CategoryTheory.Category.{v₂, u₂} (D i)] [inst_3 : (i : I) → CategoryTheory.MonoidalCategory (D i)]
  (F : (i : I) → CategoryTheory.Functor (D i) (C i)) [inst_4 : (i : I) → (F i).Monoidal] (X Y : (i : I) → D i) (i : I),
  CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Functor.pi F) X Y i =
    CategoryTheory.Functor.LaxMonoidal.μ (F i) (X i) (Y i)
-- Mathlib.Data.Int.ModEq
Int.ModEq.eq : ∀ {n a b : ℤ}, a ≡ b [ZMOD n] → a % n = b % n
-- Mathlib.Topology.Algebra.Module.LinearPMap
/-- If `f` is invertible and closable as well as its closure being invertible, then
the graph of the inverse of the closure is given by the closure of the graph of the inverse.  -/
LinearPMap.closure_inverse_graph : ∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup E] [inst_2 : AddCommGroup F]
  [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : TopologicalSpace E] [inst_6 : TopologicalSpace F]
  {f : E →ₗ.[R] F} [inst_7 : ContinuousAdd E] [inst_8 : ContinuousAdd F] [inst_9 : TopologicalSpace R]
  [inst_10 : ContinuousSMul R E] [inst_11 : ContinuousSMul R F],
  f.toFun.ker = ⊥ →
    f.IsClosable → f.closure.toFun.ker = ⊥ → f.closure.inverse.graph = f.inverse.graph.topologicalClosure
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- If the image under the norm is zero, then the argument is one.  -/
GroupNorm.eq_one_of_map_eq_zero' : ∀ {G : Type u_6} [inst : Group G] (self : GroupNorm G) (x : G), self.toFun x = 0 → x = 1
-- Mathlib.Order.Circular
btw_refl_left_right : ∀ {α : Type u_1} [inst : CircularOrder α] (a b : α), btw a b a