mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Algebra.Operations
Submodule.pow_eq_span_pow_set : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] (M : Submodule R A)
  (n : ℕ), M ^ n = Submodule.span R (↑M ^ n)
-- Std.Internal.Do.Order.Basic
Lean.Order.propSup_is_sup : ∀ (c : Prop → Prop), Lean.Order.is_sup c (Lean.Order.propSup c)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonDocumentSymbolParams.fromJson : Lean.Json → Except String Lean.Lsp.DocumentSymbolParams
-- Mathlib.Data.Set.Defs
/-- The complement of a set `s` is the set of elements not contained in `s`.

Note that you should **not** use this definition directly, but instead write `sᶜ`.  -/
Set.compl : {α : Type u} → Set α → Set α
-- Mathlib.Topology.VectorBundle.Basic
VectorPrebundle.pretrivialization_linear' : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : NontriviallyNormedField R]
  [inst_1 : (x : B) → AddCommMonoid (E x)] [inst_2 : (x : B) → Module R (E x)] [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace R F] [inst_5 : TopologicalSpace B] [inst_6 : (x : B) → TopologicalSpace (E x)]
  (self : VectorPrebundle R F E), ∀ e ∈ self.pretrivializationAtlas, Bundle.Pretrivialization.IsLinear R e
-- Init.Data.Vector.DecidableEq
Vector.beq_eq_decide : ∀ {α : Type u_1} {n : ℕ} [inst : BEq α] (xs ys : Vector α n),
  (xs == ys) = decide (∀ (i : ℕ) (h' : i < n), (xs[i] == ys[i]) = true)
-- Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
CategoryTheory.ObjectProperty.instIsMultiplicativeMonoModSerre : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsSerreClass], P.monoModSerre.IsMultiplicative
-- Init.Grind.Interactive
/-- Shows propositions known to be `True`.  -/
Lean.Parser.Tactic.Grind.showTrue : Lean.ParserDescr
-- Mathlib.CategoryTheory.EffectiveEpi.Preserves
CategoryTheory.Functor.instReflectsEffectiveEpisComp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [F.ReflectsEffectiveEpis] [G.ReflectsEffectiveEpis],
  (F.comp G).ReflectsEffectiveEpis
-- Mathlib.Algebra.Order.Group.Finset
Finset.mul_sup' : ∀ {ι : Type u_1} {G : Type u_4} [inst : Group G] [inst_1 : LinearOrder G] [MulLeftMono G] (s : Finset ι) (f : ι → G)
  (a : G) (hs : s.Nonempty), a * s.sup' hs f = s.sup' hs fun i => a * f i
-- Mathlib.CategoryTheory.Topos.Sheaf
CategoryTheory.Sheaf.classifier_χ₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  (Y : CategoryTheory.Sheaf J (Type (max u v))),
  (CategoryTheory.Sheaf.classifier J).χ₀ Y =
    (CategoryTheory.Sheaf.isTerminalTerminal J CategoryTheory.Limits.Types.isTerminalPUnit).from Y
-- Mathlib.RingTheory.Ideal.Height
/-- **Alias** of `Ideal.height_strict_mono_of_isPrime_of_isPrime`. -/
Ideal.height_strict_mono_of_isPrime_of_is_prime : ∀ {R : Type u_1} [inst : CommRing R] {I J : Ideal R} [I.IsPrime] [J.IsPrime],
  I < J → ∀ [J.FiniteHeight], I.height < J.height
-- Init.Data.Dyadic.Basic
/-- Converting a rational to a dyadic at a given precision and then back to a rational
gives the same result as taking the floor of the rational at precision `2 ^ prec`.
 -/
Rat.toRat_toDyadic : ∀ (x : ℚ) (prec : ℤ), (x.toDyadic prec).toRat = ↑(x * 2 ^ prec).floor / 2 ^ prec
-- Mathlib.Order.SuccPred.Limit
Order.IsSuccPrelimit.noMaxOrder_Iio : ∀ {α : Type u_1} {a : α} [inst : Preorder α], Order.IsSuccPrelimit a → NoMaxOrder ↑(Set.Iio a)
-- Mathlib.NumberTheory.LSeries.Convolution
/-- If we consider an arithmetic function just as a function and turn it back into an
arithmetic function, it is the same as before.  -/
ArithmeticFunction.toArithmeticFunction_eq_self : ∀ {R : Type u_1} [inst : Zero R] (f : ArithmeticFunction R), toArithmeticFunction ⇑f = f
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiff.continuous_zero : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F},
  ContDiff 𝕜 0 f → Continuous f
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullbackProdFstIsoProd_hom_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (Z : C)
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct Y Z] [inst_2 : CategoryTheory.Limits.HasBinaryProduct X Z]
  [inst_3 : CategoryTheory.Limits.HasPullback f CategoryTheory.Limits.prod.fst] {Z_1 : C} (h : Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackProdFstIsoProd f Z).hom
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f CategoryTheory.Limits.prod.fst)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h)
-- Mathlib.Algebra.Homology.LeftResolution.Basic
CategoryTheory.Abelian.LeftResolution.chainComplexXOneIso.eq_1 : ∀ {A : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} A] {ι : CategoryTheory.Functor C A}
  (Λ : CategoryTheory.Abelian.LeftResolution ι) (X : A) [inst_2 : ι.Full] [inst_3 : ι.Faithful]
  [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_5 : CategoryTheory.Abelian A],
  Λ.chainComplexXOneIso X = CategoryTheory.Iso.refl ((Λ.chainComplex X).X 1)
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
/-- **Alias** of the reverse direction of `AbsoluteValue.ne_zero_iff`. -/
AbsoluteValue.ne_zero : ∀ {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  (abv : AbsoluteValue R S) {x : R}, x ≠ 0 → abv x ≠ 0
-- Mathlib.Data.Num.ZNum
Num.cast_ofZNum : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] (n : ZNum), ↑(Num.ofZNum n) = ↑(↑n).toNat
-- Lean.EnvExtension
Lean.SimplePersistentEnvExtensionDescr.asyncMode : {α σ : Type} → Lean.SimplePersistentEnvExtensionDescr α σ → Lean.EnvExtension.AsyncMode
-- Mathlib.Geometry.Manifold.Algebra.Monoid
contMDiff_finsum : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : AddCommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffAdd I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {f : ι → M → G},
  (∀ (i : ι), ContMDiff I' I n (f i)) →
    (LocallyFinite fun i => Function.support (f i)) → ContMDiff I' I n fun x => ∑ᶠ (i : ι), f i x
-- Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy
TopCat.δ_one_toSSetObj₁Equiv.symm : ∀ {X : TopCat} (f : TopCat.I ⟶ X),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (TopCat.toSSet.obj X) 1))
      (TopCat.toSSetObj₁Equiv.symm f) =
    TopCat.toSSetObj₀Equiv.symm ((CategoryTheory.ConcreteCategory.hom f) 0)
-- Mathlib.AlgebraicGeometry.AffineScheme
/-- If `X` is affine, the image of the zero locus of global sections of `X` under `X.isoSpec`
is the zero locus in terms of the prime spectrum of `Γ(X, ⊤)`.  -/
AlgebraicGeometry.Scheme.isoSpec_image_zeroLocus : ∀ (X : AlgebraicGeometry.Scheme) [inst : AlgebraicGeometry.IsAffine X] (s : Set ↑(X.presheaf.obj (Opposite.op ⊤))),
  ⇑X.isoSpec.hom '' X.zeroLocus s = PrimeSpectrum.zeroLocus s
-- Mathlib.Tactic.NormNum.Inv
Mathlib.Meta.NormNum.isNNRat_ratCast : ∀ {R : Type u_1} [inst : DivisionRing R] [CharZero R] {q : ℚ} {n d : ℕ},
  Mathlib.Meta.NormNum.IsNNRat q n d → Mathlib.Meta.NormNum.IsNNRat (↑q) n d
-- Mathlib.Combinatorics.Configuration
/-- A nondegenerate configuration in which every pair of lines has an intersection point.  -/
Configuration.HasPoints : (P : Type u_1) → (L : Type u_2) → [Membership P L] → Type (max u_1 u_2)
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.str : (self : CommMonCat) → CommMonoid ↑self
-- Mathlib.RingTheory.Ideal.NatInt
Ideal.isPrime_nat_iff : ∀ {P : Ideal ℕ}, P.IsPrime ↔ P = ⊥ ∨ P = IsLocalRing.maximalIdeal ℕ ∨ ∃ p, Nat.Prime p ∧ P = Ideal.span {p}
-- Mathlib.Order.OrderIsoNat
/-- A strict order relation is well-founded iff it doesn't have any infinite descending chain.

See `wellFounded_iff_isEmpty_descending_chain` for a version which works on any relation.  -/
RelEmbedding.wellFounded_iff_isEmpty : ∀ {α : Type u_1} {r : α → α → Prop} [IsStrictOrder α r], WellFounded r ↔ IsEmpty ((fun x1 x2 => x1 > x2) ↪r r)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.dec.inj : ∀ {h h_1 : Lean.FVarId},
  Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.dec h = Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.dec h_1 → h = h_1
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.closure_subset_span : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s : Set M},
  ↑(AddSubmonoid.closure s) ⊆ ↑(Submodule.span R s)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.sigmaOfIsColimit_X : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) (x : PUnit.{w + 1}),
  (E.sigmaOfIsColimit hc).X x = c.pt
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
coe_basisOfLinearIndependentOfCardEqFinrank : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {ι : Type u_1}
  [inst_3 : Fintype ι] [inst_4 : Nonempty ι] {b : ι → V} (lin_ind : LinearIndependent K b)
  (card_eq : Fintype.card ι = Module.finrank K V), ⇑(basisOfLinearIndependentOfCardEqFinrank lin_ind card_eq) = b
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get!_of_isEmpty : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β],
  m.WF → ∀ {a : α}, m.isEmpty = true → Std.DHashMap.Raw.Const.get! m a = default
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
/-- An element of a DVR is irreducible iff it is a uniformizer, that is, generates the
maximal ideal of `R`.  -/
IsDiscreteValuationRing.irreducible_iff_uniformizer : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] (ϖ : R),
  Irreducible ϖ ↔ IsLocalRing.maximalIdeal R = Ideal.span {ϖ}
-- Mathlib.Algebra.Polynomial.FieldDivision
/-- Division of polynomials. See `Polynomial.divByMonic` for more details.  -/
Polynomial.div : {R : Type u} → [inst : Field R] → Polynomial R → Polynomial R → Polynomial R
-- Mathlib.Topology.ContinuousMap.Interval
ContinuousMap.IccInclusionLeft.congr_simp : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] {a b c : α} [inst_2 : Fact (b ≤ c)],
  ContinuousMap.IccInclusionLeft = ContinuousMap.IccInclusionLeft
-- Mathlib.Algebra.Group.Subgroup.Finite
MonoidHom.decidableMemRange.eq_1 : ∀ {G : Type u_1} [inst : Group G] {N : Type u_3} [inst_1 : Group N] (f : G →* N) [inst_2 : Fintype G]
  [inst_3 : DecidableEq N] (x : N), f.decidableMemRange x = Fintype.decidableExistsFintype
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.IsPrimitive.content_eq_one : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : NormalizedGCDMonoid R] {p : Polynomial R}, p.IsPrimitive → p.content = 1
-- Init.Data.List.MinMax
List.max?_eq_some_iff_subtype : ∀ {α : Type u_1} {a : α} [inst : Max α] [inst_1 : LE α] {xs : List α} [inst_2 : Std.MaxEqOr α]
  [Std.IsLinearOrder { x // x ∈ xs }] [Std.LawfulOrderMax { x // x ∈ xs }], xs.max? = some a ↔ a ∈ xs ∧ ∀ b ∈ xs, b ≤ a
-- Mathlib.Data.Finset.Basic
Finset.filter_cons : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] {a : α} (s : Finset α) (ha : a ∉ s),
  Finset.filter p (Finset.cons a s ha) = if p a then Finset.cons a (Finset.filter p s) ⋯ else Finset.filter p s
-- Mathlib.Order.Filter.IsBounded
Filter.isBounded_sup : ∀ {α : Type u_1} {r : α → α → Prop} {f g : Filter α} [IsTrans α r] [IsDirected α r],
  Filter.IsBounded r f → Filter.IsBounded r g → Filter.IsBounded r (f ⊔ g)
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
SSet.StrictSegal.spineToSimplex_vertex : ∀ {X : SSet} (sx : X.StrictSegal) {n : ℕ} (i : Fin (n + 1)) (f : X.Path n),
  (CategoryTheory.ConcreteCategory.hom (X.map ({ len := 0 }.const { len := n } i).op)) (sx.spineToSimplex f) =
    f.vertex i
-- Mathlib.Order.Category.BddLat
/-- Constructs an equivalence between bounded lattices from an order isomorphism
between them.  -/
BddLat.Iso.mk : {α β : BddLat} → ↑α.toLat ≃o ↑β.toLat → (α ≅ β)
-- Mathlib.Order.WellFoundedSet
Set.IsWF.min_of_subset_not_lt_min : ∀ {α : Type u_2} [inst : Preorder α] {s t : Set α} {hs : s.IsWF} {hsn : s.Nonempty} {ht : t.IsWF} {htn : t.Nonempty},
  s ⊆ t → ¬hs.min hsn < ht.min htn
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- An arbitrary choice of colimit cocone of a functor.  -/
CategoryTheory.Limits.colimit.cocone : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        (F : CategoryTheory.Functor J C) → [CategoryTheory.Limits.HasColimit F] → CategoryTheory.Limits.Cocone F
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_insert : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x : M)
  (s : Set M), Submodule.span R (insert x s) = R ∙ x ⊔ Submodule.span R s
-- Mathlib.Order.WithBot
WithTop.trichotomous.lt : ∀ {α : Type u_1} [inst : Preorder α] [Std.Trichotomous fun x1 x2 => x1 < x2], Std.Trichotomous fun x1 x2 => x1 < x2
-- Std.Data.DTreeMap.Basic
/-- Folds the given function over the mappings in the map in descending order.  -/
Std.DTreeMap.foldr : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → {δ : Type w} → ((a : α) → β a → δ → δ) → δ → Std.DTreeMap α β cmp → δ
-- Mathlib.Topology.Inseparable
Specializes.map_of_continuousWithinAt : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x y : X} {f : X → Y}
  {s : Set X}, x ⤳ y → ContinuousWithinAt f s y → x ∈ s → f x ⤳ f y
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
/-- Transport evidence that a left lift is a Kan lift across an isomorphism of lifts.  -/
CategoryTheory.Bicategory.LeftLift.IsKan.ofIsoKan : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : b ⟶ a} → {g : c ⟶ a} → {s t : CategoryTheory.Bicategory.LeftLift f g} → s.IsKan → (s ≅ t) → t.IsKan
-- Init.Data.SInt.Lemmas
Int32.neg_sub : ∀ {a b : Int32}, -(a - b) = b - a
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
/-- A function is `C^n` at a point iff it is `C^m` at this point, for
any `m ≤ n` which is different from `∞`. This result is useful because, when `m ≠ ∞`, being
`C^m` extends locally to a neighborhood, giving flexibility for local proofs.  -/
contMDiffAt_iff_le_ne_infty : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {n : WithTop ℕ∞},
  ContMDiffAt I I' n f x ↔ ∀ m ≤ n, m ≠ ↑⊤ → ContMDiffAt I I' m f x
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_pair_sub_left_mul : ∀ {α : Type u} [inst : CommRing α] (x y z : α), Ideal.span {x, y - x * z} = Ideal.span {x, y}
-- Mathlib.CategoryTheory.Elementwise
CategoryTheory.Iso.inv_hom_id_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (self : X ≅ Y) {F : C → C → Type uF}
  {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)}
  [inst_1 : CategoryTheory.ConcreteCategory C F] (x : carrier Y),
  (CategoryTheory.ConcreteCategory.hom self.hom) ((CategoryTheory.ConcreteCategory.hom self.inv) x) = x
-- Init.Data.BitVec.Lemmas
BitVec.getElem_ofBool : ∀ {i : ℕ} {b : Bool} {h : i < 1}, (BitVec.ofBool b)[i] = b
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
UniformCauchySeqOn.neg : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Type u_3}
  {l : Filter ι} {f : ι → β → α} {s : Set β}, UniformCauchySeqOn f l s → UniformCauchySeqOn (-f) l s
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
le_ciSup_ciSup_eq_left : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] {b : β} {f : (x : β) → x = b → α},
  f b ⋯ ≤ ⨆ x, ⨆ (h : x = b), f x h
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Sigma.ι_isoColimit_inv_assoc : ∀ {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C)
  [inst_1 : CategoryTheory.Limits.HasCoproduct fun j => X.obj { as := j }] [inst_2 : CategoryTheory.Limits.HasColimit X]
  (j : α) {Z : C} (h : (∐ fun j => X.obj { as := j }) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι X { as := j })
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.isoColimit X).inv h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun j => X.obj { as := j }) j) h
-- Mathlib.GroupTheory.DivisibleHull
DivisibleHull.instIsStrictOrderedModuleNNRat : ∀ {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedCancelAddMonoid M],
  IsStrictOrderedModule ℚ≥0 (DivisibleHull M)
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoid.End.instMonoid : (M : Type u_4) → [inst : AddZero M] → Monoid (AddMonoid.End M)
-- Lean.Meta.Sym.AlphaShareBuilder
Lean.Meta.Sym.Internal.mkAppS : {m : Type → Type} → [Lean.Meta.Sym.Internal.MonadShareCommon m] → [Monad m] → Lean.Expr → Lean.Expr → m Lean.Expr
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
/-- The notation `\textf` for `WeierstrassCurve.Affine.baseChange W S`.  -/
WeierstrassCurve.Affine.«term_⁄_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Localization.HomEquiv
/-- If `Φ : LocalizerMorphism W₁ W₂` is a morphism of localizers, `L₁` and `L₂`
are localization functors for `W₁` and `W₂`, then this is the induced map
`(L₁.obj X ⟶ L₁.obj Y) ⟶ (L₂.obj (Φ.functor.obj X) ⟶ L₂.obj (Φ.functor.obj Y))`
for all objects `X` and `Y`.  -/
CategoryTheory.LocalizerMorphism.homMap : {C₁ : Type u_2} →
  {C₂ : Type u_3} →
    {D₁ : Type u_5} →
      {D₂ : Type u_6} →
        [inst : CategoryTheory.Category.{v_2, u_2} C₁] →
          [inst_1 : CategoryTheory.Category.{v_3, u_3} C₂] →
            [inst_2 : CategoryTheory.Category.{v_5, u_5} D₁] →
              [inst_3 : CategoryTheory.Category.{v_6, u_6} D₂] →
                {W₁ : CategoryTheory.MorphismProperty C₁} →
                  {W₂ : CategoryTheory.MorphismProperty C₂} →
                    (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) →
                      (L₁ : CategoryTheory.Functor C₁ D₁) →
                        [L₁.IsLocalization W₁] →
                          (L₂ : CategoryTheory.Functor C₂ D₂) →
                            [L₂.IsLocalization W₂] →
                              {X Y : C₁} → (L₁.obj X ⟶ L₁.obj Y) → (L₂.obj (Φ.functor.obj X) ⟶ L₂.obj (Φ.functor.obj Y))
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instDivInvMonoid : {α : Type u_1} → [DivInvMonoid α] → DivInvMonoid (Colex α)
-- Mathlib.Order.Filter.Basic
Filter.Frequently.exists : ∀ {α : Type u} {p : α → Prop} {f : Filter α}, (∃ᶠ (x : α) in f, p x) → ∃ x, p x
-- Init.Data.Vector.Attach
Vector.findSome?_subtype : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {p : α → Prop} {xs : Vector { x // p x } n} {f : { x // p x } → Option β}
  {g : α → Option β}, (∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) → Vector.findSome? f xs = Vector.findSome? g xs.unattach
-- Mathlib.Geometry.Manifold.Algebra.Monoid
contMDiffWithinAt_finsetProd' : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : CommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffMul I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {s : Set M} {x : M} {t : Finset ι}
  {f : ι → M → G}, (∀ i ∈ t, ContMDiffWithinAt I' I n (f i) s x) → ContMDiffWithinAt I' I n (∏ i ∈ t, f i) s x
-- Mathlib.CategoryTheory.Limits.Set
Set.instPreservesColimitsOfShapeFunctorToTypesOfIsFilteredOrEmpty : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {X : Type u} [CategoryTheory.IsFilteredOrEmpty J],
  CategoryTheory.Limits.PreservesColimitsOfShape J Set.functorToTypes
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get!_filterMap : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {γ : α → Type w}
  [inst : LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {k : α} [inst_1 : Inhabited (γ k)],
  (Std.DHashMap.filterMap f m).get! k = ((m.get? k).bind (f k)).get!
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
CategoryTheory.Lax.LaxTrans.isoMk_hom_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} {η θ : F ⟶ G} (app : (a : B) → η.app a ≅ θ.app a)
  (naturality :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (app a).hom (G.map f))
            (θ.naturality f) =
          CategoryTheory.CategoryStruct.comp (η.naturality f)
            (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b).hom))
      CategoryTheory.Lax.LaxTrans.isoMk._auto_1)
  (a : B), (CategoryTheory.Lax.LaxTrans.isoMk app naturality).hom.as.app a = (app a).hom
-- Mathlib.Data.Ordmap.Invariants
Ordnode.node'.eq_1 : ∀ {α : Type u_1} (l : Ordnode α) (x : α) (r : Ordnode α), l.node' x r = Ordnode.node (l.size + r.size + 1) l x r
-- Init.Data.Order.Classes
Std.LawfulOrderLeftLeaningMin.mk : ∀ {α : Type u} [inst : Min α] [inst_1 : LE α],
  (∀ (a b : α), a ≤ b → a ⊓ b = a) → (∀ (a b : α), ¬a ≤ b → a ⊓ b = b) → Std.LawfulOrderLeftLeaningMin α
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey!_inter_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {k : α}, k ∉ m₁ → (m₁ ∩ m₂).getKey! k = default
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSet.iUnion : ∀ {α : Type u_1} {ι : Sort u_6} {m : MeasurableSpace α} [Countable ι] ⦃f : ι → Set α⦄,
  (∀ (b : ι), MeasurableSet (f b)) → MeasurableSet (⋃ b, f b)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.keys_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} {f : α → β → γ},
  (Std.TreeMap.Raw.map f t).keys = t.keys
-- Mathlib.Algebra.QuaternionBasis
/-- The first imaginary unit  -/
QuaternionAlgebra.Basis.i : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : Ring A] → [inst_2 : Algebra R A] → {c₁ c₂ c₃ : R} → QuaternionAlgebra.Basis A c₁ c₂ c₃ → A
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.FoldingRangeKind.imports : Lean.Lsp.FoldingRangeKind
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- Expressions for atomic 1-morphisms.  -/
Mathlib.Tactic.BicategoryLike.Atom₁ : Type