mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_alter! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {k k' : α} {f : Option (β k) → Option (β k)},
      Std.DTreeMap.Internal.Impl.contains k' (Std.DTreeMap.Internal.Impl.alter! k f t) =
        if compare k k' = Ordering.eq then (f (t.get? k)).isSome else Std.DTreeMap.Internal.Impl.contains k' t
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
neg_of_add_lt_right : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LT α] [AddLeftReflectLT α] {a b : α}, a + b < a → b < 0
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas
_private.Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas.0.RootPairing.chainBotCoeff_mul_chainTopCoeff.aux_1 : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : CharZero R]
  [inst_2 : IsDomain R] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : AddCommGroup N] [inst_6 : Module R N]
  {P : RootPairing ι R M N} [inst_7 : Finite ι] [inst_8 : P.IsCrystallographic] {b : P.Base} {i j k l m : ι}
  [P.IsReduced] [P.IsIrreducible],
  i ∈ b.support →
    j ∈ b.support →
      i ≠ j →
        P.root k + P.root i = P.root l →
          P.root k - P.root j = P.root m →
            P.root k + P.root i - P.root j ∈ Set.range ⇑P.root →
              P.pairingIn ℤ k i = 0 →
                have this := ⋯;
                P.root i + P.root m ∈ Set.range ⇑P.root →
                  P.root j + P.root (-l) ∈ Set.range ⇑P.root →
                    P.root j + P.root (-k) ∈ Set.range ⇑P.root →
                      (RootPairing.chainBotCoeff i m + 1) * (RootPairing.chainBotCoeff j (-k) + 1) =
                        (RootPairing.chainBotCoeff j (-l) + 1) * (RootPairing.chainBotCoeff i k + 1)
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
MeasureTheory.VectorMeasure.variation.congr_simp : ∀ {X : Type u_1} {mX : MeasurableSpace X} {V : Type u_2} [inst : TopologicalSpace V] [inst_1 : ENormedAddCommMonoid V]
  [inst_2 : T2Space V] (μ μ_1 : MeasureTheory.VectorMeasure X V), μ = μ_1 → μ.variation = μ_1.variation
-- Mathlib.Logic.Equiv.Basic
Equiv.swap_swap : ∀ {α : Sort u_1} [inst : DecidableEq α] (a b : α), Equiv.trans (Equiv.swap a b) (Equiv.swap a b) = Equiv.refl α
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.const_add_termg : ∀ {α : Type u_1} [inst : AddCommGroup α] (k : α) (n : ℤ) (x a a' : α),
  k + a = a' → k + Mathlib.Tactic.Abel.termg n x a = Mathlib.Tactic.Abel.termg n x a'
-- Mathlib.CategoryTheory.Join.Pseudofunctor
CategoryTheory.Join.mapWhiskerLeft_rightUnitor_hom : ∀ (A : Type u_1) {B : Type u_2} {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  (F : CategoryTheory.Functor B C),
  CategoryTheory.Join.mapWhiskerLeft (CategoryTheory.Functor.id A) F.rightUnitor.hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Join.mapCompRight A F (CategoryTheory.Functor.id C)).hom
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Join.mapPair (CategoryTheory.Functor.id A) F).whiskerLeft CategoryTheory.Join.mapPairId.hom)
        (CategoryTheory.Join.mapPair (CategoryTheory.Functor.id A) F).rightUnitor.hom)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_erase! : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α}
  {l : Std.DTreeMap.Internal.Impl α β},
  l.Balanced →
    l.Ordered → (Std.DTreeMap.Internal.Impl.erase! k l).toListModel.Perm (Std.Internal.List.eraseKey k l.toListModel)
-- Mathlib.RingTheory.HopfAlgebra.Convolution
_private.Mathlib.RingTheory.HopfAlgebra.Convolution.0.LinearMap.«term𝑺» : Lean.ParserDescr
-- Mathlib.Topology.Algebra.Group.Pointwise
IsOpen.closure_add : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] {t : Set G},
  IsOpen t → ∀ (s : Set G), closure s + t = s + t
-- Mathlib.Condensed.Light.Sequence
_private.Mathlib.Condensed.Light.Sequence.0.InternalProjectivityProof.fibreIncl : {S : Type u_1} →
  {T : Type u_2} →
    {X : Type u_3} →
      (π : T → S × Option X) →
        (σ : Option X → S → T) →
          ↑(Prod.snd ∘ InternalProjectivityProof.π_r✝ π σ ⁻¹' {none}) → ↑(InternalProjectivityProof.fibres✝ π σ)
-- Init.System.IOError
IO.Error.otherError.inj : ∀ {osCode : UInt32} {details : String} {osCode_1 : UInt32} {details_1 : String},
  IO.Error.otherError osCode details = IO.Error.otherError osCode_1 details_1 → osCode = osCode_1 ∧ details = details_1
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_minKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {km : α}, t.minKey? = some km → t.getKey? km = some km
-- Init.Data.SInt.Lemmas
Int64.toInt_neg : ∀ (n : Int64), (-n).toInt = (-n.toInt).bmod (2 ^ 64)
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
UniformOnFun.isCountablyGenerated_uniformity : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace β] (𝔖 : Set (Set α)) [(uniformity β).IsCountablyGenerated]
  {t : ℕ → Set α},
  (∀ (n : ℕ), t n ∈ 𝔖) → Monotone t → (∀ s ∈ 𝔖, ∃ n, s ⊆ t n) → (uniformity (UniformOnFun α β 𝔖)).IsCountablyGenerated
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.support_takeUntil_subset_support : ∀ {V : Type u} {G : SimpleGraph V} {v w u : V} [inst : DecidableEq V] (p : G.Walk v w) (h : u ∈ p.support),
  (p.takeUntil u h).support ⊆ p.support
-- Mathlib.Data.Complex.Basic
Complex.normSq_add_mul_I : ∀ (x y : ℝ), Complex.normSq (↑x + ↑y * Complex.I) = x ^ 2 + y ^ 2
-- Mathlib.Order.Heyting.Basic
sup_himp_self_right : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] (a b : α), a ⊔ b ⇨ b = a ⇨ b
-- Mathlib.Topology.Algebra.Support
mulTSupport_one : ∀ {X : Type u_1} {α : Type u_2} [inst : One α] [inst_1 : TopologicalSpace X], mulTSupport 1 = ∅
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F.unop : C ⥤ D` creates colimits, then `F : Cᵒᵖ ⥤ Dᵒᵖ` creates limits.  -/
CategoryTheory.Limits.createsLimitsOfUnop : {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.CreatesColimits F.unop] → CategoryTheory.CreatesLimits F
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Decl.mk.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {toSignature : Lean.Compiler.LCNF.Signature pu}
  {value : Lean.Compiler.LCNF.DeclValue pu} {recursive : Bool} {inlineAttr? : Option Lean.Compiler.InlineAttributeKind}
  {toSignature_1 : Lean.Compiler.LCNF.Signature pu} {value_1 : Lean.Compiler.LCNF.DeclValue pu} {recursive_1 : Bool}
  {inlineAttr?_1 : Option Lean.Compiler.InlineAttributeKind},
  { toSignature := toSignature, value := value, recursive := recursive, inlineAttr? := inlineAttr? } =
      { toSignature := toSignature_1, value := value_1, recursive := recursive_1, inlineAttr? := inlineAttr?_1 } →
    toSignature = toSignature_1 ∧ value = value_1 ∧ recursive = recursive_1 ∧ inlineAttr? = inlineAttr?_1
-- Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
Algebra.GrothendieckGroup.of_injective : ∀ {M : Type u_1} [inst : CommMonoid M] [IsCancelMul M], Function.Injective ⇑Algebra.GrothendieckGroup.of
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.map_of : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (x : α), (FreeAddMonoid.map f) (FreeAddMonoid.of x) = FreeAddMonoid.of (f x)
-- Init.Data.Int.DivMod.Lemmas
Int.tmod_one : ∀ (a : ℤ), a.tmod 1 = 0
-- Aesop.Util.UnorderedArraySet
/-- O(1)  -/
Aesop.UnorderedArraySet.size : {α : Type u_1} → [inst : BEq α] → Aesop.UnorderedArraySet α → ℕ
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pullback_lift_map_isPullback : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {X Y S X' Y' S' : C} (f : X ⟶ S) (g : Y ⟶ S) (f' : X' ⟶ S') (g' : Y' ⟶ S') (i₁ : X ⟶ X') (i₂ : Y ⟶ Y') (i₃ : S ⟶ S')
  (e₁ : CategoryTheory.CategoryStruct.comp f i₃ = CategoryTheory.CategoryStruct.comp i₁ f')
  (e₂ : CategoryTheory.CategoryStruct.comp g i₃ = CategoryTheory.CategoryStruct.comp i₂ g') [CategoryTheory.Mono i₃],
  CategoryTheory.IsPullback
    (CategoryTheory.Limits.pullback.lift (CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂)
      (CategoryTheory.Limits.pullback.fst f g) ⋯)
    (CategoryTheory.Limits.pullback.lift (CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂)
      (CategoryTheory.Limits.pullback.snd f g) ⋯)
    (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst f' g') i₁)
    (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd f' g') i₂)
-- Mathlib.Analysis.Normed.Group.BallSphere
coe_neg_closedBall : ∀ {E : Type u_1} [i : SeminormedAddCommGroup E] {r : ℝ} (v : ↑(Metric.closedBall 0 r)), ↑(-v) = -↑v
-- Mathlib.Analysis.Convex.Topology
Convex.Ioo_subset_of_mem_closure : ∀ {𝕜 : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [OrderTopology 𝕜] {s : Set 𝕜}, Convex 𝕜 s → ∀ {a b : 𝕜}, a ∈ closure s → b ∈ closure s → Set.Ioo a b ⊆ s
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.coverEntropyInf_empty : ∀ {X : Type u_1} {T : X → X} [inst : UniformSpace X], Dynamics.coverEntropyInf T ∅ = ⊥
-- Mathlib.Algebra.Order.IsBotOne
isBot_zero : ∀ {α : Type u_1} [inst : LE α] [inst_1 : Zero α] [IsBotZeroClass α], IsBot 0
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
/-- **Alias** of the reverse direction of `NumberField.ComplexEmbedding.isConj_one_iff`. -/
NumberField.ComplexEmbedding.IsReal.isConjGal_one : ∀ {K : Type u_1} [inst : Field K] {k : Type u_2} [inst_1 : Field k] [inst_2 : Algebra k K] {φ : K →+* ℂ},
  NumberField.ComplexEmbedding.IsReal φ → NumberField.ComplexEmbedding.IsConj φ 1
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapAddGrpFunctor_map_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {F G : C ⥤ₗ D} (α : F ⟶ G) (A : CategoryTheory.AddGrp C),
  (CategoryTheory.Functor.mapAddGrpFunctor.map α).app A = CategoryTheory.AddGrp.homMk'' (α.hom.app A.X) ⋯ ⋯
-- Mathlib.Data.Matrix.Mul
/-- `dotProduct v w` is the sum of the entrywise products `v i * w i`.

See also `dotProductEquiv`.  -/
dotProduct : {m : Type u_2} → {α : Type v} → [Fintype m] → [Mul α] → [AddCommMonoid α] → (m → α) → (m → α) → α
-- Mathlib.CategoryTheory.Subfunctor.Finite
/-- A choice of generating sections of a finitely generated subpresheaf.  -/
CategoryTheory.Subfunctor.IsFinite.x : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor Cᵒᵖ (Type w)} →
      {G : CategoryTheory.Subfunctor F} →
        [hG : G.IsFinite] →
          (i : CategoryTheory.Subfunctor.IsFinite.Index G) → F.obj (CategoryTheory.Subfunctor.IsFinite.X i)
-- Mathlib.Algebra.Order.Ring.Ordering.Basic
RingPreordering.HasIdealSupport.neg_smul_mem : ∀ {R : Type u_1} [inst : CommRing R] {P : RingPreordering R} [P.HasIdealSupport] (x : R) {a : R},
  a ∈ P → -a ∈ P → -(x * a) ∈ P
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.IterM.DefaultConsumers.forIn'.match_1.splitter : {β : Type u_3} →
  (γ : Type u_1) →
    (PlausibleForInStep : β → γ → ForInStep γ → Prop) →
      (acc : γ) →
        (out : β) →
          (motive : Subtype (PlausibleForInStep out acc) → Sort u_2) →
            (__do_lift : Subtype (PlausibleForInStep out acc)) →
              ((c : γ) → (h' : PlausibleForInStep out acc (ForInStep.yield c)) → motive ⟨ForInStep.yield c, h'⟩) →
                ((c : γ) → (h : PlausibleForInStep out acc (ForInStep.done c)) → motive ⟨ForInStep.done c, h⟩) →
                  motive __do_lift
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.instInhabitedState.default : Lean.Meta.Grind.Arith.CommRing.State
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
/-- If `m` is a monad, then `HetT m` is a monad that has two features:

* It generalizes `m` to arbitrary universes.
* It tracks a postcondition property that holds for the monadic return value, similarly to
  `PostconditionT`.

This monad is noncomputable and is merely a vehicle for more convenient proofs, especially proofs
about the equivalence of iterators, because it avoids universe issues and spares users the work
to handle the postconditions manually.

Caution: Just like `PostconditionT`, this is not a lawful monad transformer.
To lift from `m` to `HetT m`, use `HetT.lift`.

Because this monad is fundamentally universe-polymorphic, it is recommended for consistency to
always use the methods `HetT.pure`, `HetT.map` and `HetT.bind` instead of the homogeneous versions
`Pure.pure`, `Functor.map` and `Bind.bind`.
 -/
Std.Iterators.HetT : (Type w → Type w') → Type v → Type (max v w')
-- Mathlib.Order.Cover
Set.sdiff_singleton_wcovBy : ∀ {α : Type u_1} (s : Set α) (a : α), s \ {a} ⩿ s
-- Mathlib.Data.ENNReal.Inv
ENNReal.div_pos : ∀ {a b : ENNReal}, a ≠ 0 → b ≠ ⊤ → 0 < a / b
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.ObjectProperty.zero_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (P : CategoryTheory.ObjectProperty C) (X Y : P.FullSubcategory), CategoryTheory.InducedCategory.Hom.hom 0 = 0
-- Mathlib.Analysis.Complex.HalfPlane
/-- An open upper half-plane (with boundary imaginary part given by an `EReal`) is an open set
in the complex plane.  -/
Complex.isOpen_im_gt_EReal : ∀ (x : EReal), IsOpen {z | x < ↑z.im}
-- Lean.Elab.Quotation
_private.Lean.Elab.Quotation.0.Lean.Elab.Term.Quotation.getSepFromSplice : Lean.Syntax → String
-- Mathlib.Topology.Compactness.Compact
Set.Infinite.exists_accPt_principal : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} [CompactSpace X], s.Infinite → ∃ x, AccPt x (Filter.principal s)
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsFundamentalDomain.hasFiniteIntegral_on_iff : ∀ {G : Type u_1} {α : Type u_3} {E : Type u_5} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α]
  [inst_3 : NormedAddCommGroup E] {s t : Set α} {μ : MeasureTheory.Measure α} [MeasurableConstSMul G α]
  [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G],
  MeasureTheory.IsFundamentalDomain G s μ →
    MeasureTheory.IsFundamentalDomain G t μ →
      ∀ {f : α → E},
        (∀ (g : G) (x : α), f (g • x) = f x) →
          (MeasureTheory.HasFiniteIntegral f (μ.restrict s) ↔ MeasureTheory.HasFiniteIntegral f (μ.restrict t))
-- Batteries.Data.List.Perm
List.Subperm.subset : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Subperm l₂ → l₁ ⊆ l₂
-- Lean.Meta.Tactic.Grind.Types
/-- Clean name generator.  -/
Lean.Meta.Grind.Clean.State : Type
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Pattern.toMessageData : Lean.Meta.Match.Pattern → Lean.MessageData
-- Lean.Meta.Basic
/-- Controls which definitions and theorems can be unfolded by `isDefEq` and `whnf`.
 -/
Lean.Meta.Config.transparency : Lean.Meta.Config → Lean.Meta.TransparencyMode
-- Mathlib.Probability.Decision.Risk.Countable
ProbabilityTheory.avgRisk_const_of_countable : ∀ {Θ : Type u_1} {𝓧 : Type u_3} {𝓨 : Type u_5} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} [Countable 𝓨] [MeasurableSingletonClass 𝓨],
  Measurable ℓ →
    ∀ (μ : MeasureTheory.Measure 𝓧) (κ : ProbabilityTheory.Kernel 𝓧 𝓨) (π : MeasureTheory.Measure Θ),
      ProbabilityTheory.avgRisk ℓ (ProbabilityTheory.Kernel.const Θ μ) κ π =
        ∑' (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y * (μ.bind ⇑κ) {y} ∂π
-- Mathlib.Data.Set.Monotone
Set.EqOn.congr_antitoneOn : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ : α → β} [inst : Preorder α] [inst_1 : Preorder β],
  Set.EqOn f₁ f₂ s → (AntitoneOn f₁ s ↔ AntitoneOn f₂ s)
-- Mathlib.Topology.Sheaves.MayerVietoris
Opens.mayerVietorisSquare'_toSquare : ∀ {T : Type u} [inst : TopologicalSpace T] (sq : CategoryTheory.Square (TopologicalSpace.Opens T))
  (h₄ : sq.X₄ = sq.X₂ ⊔ sq.X₃) (h₁ : sq.X₁ = sq.X₂ ⊓ sq.X₃), (Opens.mayerVietorisSquare' sq h₄ h₁).toSquare = sq
-- Mathlib.Data.Finset.Insert
Finset.cons_empty : ∀ {α : Type u_1} (a : α), Finset.cons a ∅ ⋯ = {a}
-- Mathlib.Analysis.Convex.Body
/-- A convex body has convex carrier set  -/
ConvexBody.convex' : ∀ {V : Type u_2} [inst : TopologicalSpace V] [inst_1 : AddCommMonoid V] [inst_2 : SMul ℝ V] (self : ConvexBody V),
  Convex ℝ self.carrier
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothPartitionOfUnity.contMDiff_smul : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {F : Type uF}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {H : Type uH} [inst_4 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_5 : TopologicalSpace M] [inst_6 : ChartedSpace H M] {s : Set M}
  (f : SmoothPartitionOfUnity ι I M s) {n : ℕ∞} {g : M → F} {i : ι},
  (∀ x ∈ tsupport ⇑(f i), ContMDiffAt I (modelWithCornersSelf ℝ F) (↑n) g x) →
    ContMDiff I (modelWithCornersSelf ℝ F) ↑n fun x => (f i) x • g x
-- Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
AddChar.exists_apply_ne_zero : ∀ {α : Type u_1} [inst : AddCommGroup α] {a : α} [Finite α], (∃ ψ, ψ a ≠ 1) ↔ a ≠ 0
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.nameLitNoAntiquot.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField
AlgebraicGeometry.LocallyRingedSpace.residueFieldMap_comp : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) {Z : AlgebraicGeometry.LocallyRingedSpace} (g : Y ⟶ Z)
  (x : ↑X.toTopCat),
  AlgebraicGeometry.LocallyRingedSpace.residueFieldMap (CategoryTheory.CategoryStruct.comp f g) x =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.LocallyRingedSpace.residueFieldMap g ((CategoryTheory.ConcreteCategory.hom f.base) x))
      (AlgebraicGeometry.LocallyRingedSpace.residueFieldMap f x)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
RingHom.domRestrict_comp_codRestrict : ∀ {R : Type u} {S : Type v} {T : Type w} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S]
  [inst_2 : NonAssocSemiring T] (g : S →+* T) (f : R →+* S) (p : Subsemiring S) (h : ∀ (c : R), f c ∈ p),
  (g.domRestrict p).comp (f.codRestrict p h) = g.comp f
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
/-- The Weierstrass curve in affine coordinates mapped over a ring homomorphism `f : R →+* S`.  -/
WeierstrassCurve.Affine.map : {R : Type r} →
  [inst : CommRing R] →
    WeierstrassCurve.Affine R → {S : Type s} → [inst_1 : CommRing S] → (R →+* S) → WeierstrassCurve.Affine S
-- Batteries.Data.Vector.Lemmas
Vector.scanr_push : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {init : β} {f : α → β → β} {as : Vector α n} {a : α},
  Vector.scanr f init (as.push a) = (Vector.scanr f (f a init) as).push init
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
/-- A limit (over a general filter) of measurable `ℝ≥0∞`-valued functions is measurable.  -/
ENNReal.measurable_of_tendsto' : ∀ {α : Type u_1} {mα : MeasurableSpace α} {ι : Type u_5} {f : ι → α → ENNReal} {g : α → ENNReal} (u : Filter ι)
  [u.NeBot] [u.IsCountablyGenerated], (∀ (i : ι), Measurable (f i)) → Filter.Tendsto f u (nhds g) → Measurable g
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
/-- Product of affine spaces is commutative up to affine isomorphism.  -/
AffineEquiv.prodComm : (k : Type u_1) →
  (P₁ : Type u_2) →
    (P₂ : Type u_3) →
      {V₁ : Type u_6} →
        {V₂ : Type u_7} →
          [inst : Ring k] →
            [inst_1 : AddCommGroup V₁] →
              [inst_2 : AddCommGroup V₂] →
                [inst_3 : Module k V₁] →
                  [inst_4 : Module k V₂] →
                    [inst_5 : AddTorsor V₁ P₁] → [inst_6 : AddTorsor V₂ P₂] → P₁ × P₂ ≃ᵃ[k] P₂ × P₁
-- Mathlib.Order.WithBot
WithTop.map₂_eq_top_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {a : WithTop α} {b : WithTop β},
  WithTop.map₂ f a b = ⊤ ↔ a = ⊤ ∨ b = ⊤
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Problem.vars : Lean.Meta.Match.Problem → List Lean.Expr
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Finsupp.linearCombination_apply_of_mem_supported : ∀ {α : Type u_1} {M : Type u_2} (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {v : α → M} {l : α →₀ R} {s : Finset α},
  l ∈ Finsupp.supported R R ↑s → (Finsupp.linearCombination R v) l = ∑ i ∈ s, l i • v i
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.homOfLE_ι : ∀ (X : AlgebraicGeometry.Scheme) {U V : X.Opens} (e : U ≤ V), CategoryTheory.CategoryStruct.comp (X.homOfLE e) V.ι = U.ι
-- Lean.Elab.Tactic.Omega.Frontend
Lean.Elab.Tactic.Omega.MetaProblem.instInhabited : Inhabited Lean.Elab.Tactic.Omega.MetaProblem
-- Mathlib.Algebra.Group.ModEq
/-- **Alias** of the forward direction of `AddCommGroup.nsmul_modEq_nsmul`. -/
AddCommGroup.ModEq.nsmul_cancel : ∀ {M : Type u_1} [inst : AddCommMonoid M] {a b p : M} [IsAddTorsionFree M] {n : ℕ},
  n ≠ 0 → n • a ≡ n • b [PMOD n • p] → a ≡ b [PMOD p]
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.instInhabitedLazyEntry.default : Lean.Meta.RefinedDiscrTree.LazyEntry
-- Mathlib.RingTheory.Unramified.Locus
Algebra.IsUnramifiedAt.comp : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra A B] [inst_5 : Algebra R B] [IsScalarTower R A B] (p : Ideal A) (P : Ideal B)
  [P.LiesOver p] [inst_8 : p.IsPrime] [inst_9 : P.IsPrime] [Algebra.IsUnramifiedAt R p] [Algebra.IsUnramifiedAt A P],
  Algebra.IsUnramifiedAt R P
-- Mathlib.LinearAlgebra.TensorProduct.Tower
/-- Heterobasic version of `TensorProduct.assoc`:

`B`-linear equivalence between `(M ⊗[A] P) ⊗[R] Q` and `M ⊗[A] (P ⊗[R] Q)`.

Note this is especially useful with `A = R` (where it is a "more linear" version of
`TensorProduct.assoc`), or with `B = A`.  -/
TensorProduct.AlgebraTensorModule.assoc : (R : Type uR) →
  (A : Type uA) →
    (B : Type uB) →
      (M : Type uM) →
        (P : Type uP) →
          (Q : Type uQ) →
            [inst : CommSemiring R] →
              [inst_1 : CommSemiring A] →
                [inst_2 : Semiring B] →
                  [inst_3 : Algebra R A] →
                    [inst_4 : Algebra R B] →
                      [inst_5 : AddCommMonoid M] →
                        [inst_6 : Module R M] →
                          [inst_7 : Module A M] →
                            [inst_8 : Module B M] →
                              [inst_9 : IsScalarTower R A M] →
                                [inst_10 : IsScalarTower R B M] →
                                  [inst_11 : SMulCommClass A B M] →
                                    [inst_12 : AddCommMonoid P] →
                                      [inst_13 : Module A P] →
                                        [inst_14 : AddCommMonoid Q] →
                                          [inst_15 : Module R Q] →
                                            [inst_16 : Module R P] →
                                              [inst_17 : IsScalarTower R A P] →
                                                [inst_18 : Algebra A B] →
                                                  [IsScalarTower A B M] →
                                                    TensorProduct R (TensorProduct A M P) Q ≃ₗ[B]
                                                      TensorProduct A M (TensorProduct R P Q)
-- Mathlib.NumberTheory.Cyclotomic.Basic
instIsDomainCyclotomicRing : ∀ (n : ℕ) (A : Type u_2) (K : Type u_1) [inst : CommRing A] [inst_1 : Field K] [inst_2 : Algebra A K],
  IsDomain (CyclotomicRing n A K)
-- Init.PropLemmas
exists_prop' : ∀ {α : Sort u_1} {p : Prop}, (∃ x, p) ↔ Nonempty α ∧ p