mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
/-- Constructor for pseudofunctors from a locally discrete bicategory. In that
case, we do not need to provide the `map₂` field of pseudofunctors.  -/
CategoryTheory.LocallyDiscrete.mkPseudofunctor : {B₀ : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} B₀] →
      [inst_1 : CategoryTheory.Bicategory C] →
        (obj : B₀ → C) →
          (map : {b b' : B₀} → (b ⟶ b') → (obj b ⟶ obj b')) →
            (mapId : (b : B₀) → map (CategoryTheory.CategoryStruct.id b) ≅ CategoryTheory.CategoryStruct.id (obj b)) →
              (mapComp :
                  {b₀ b₁ b₂ : B₀} →
                    (f : b₀ ⟶ b₁) →
                      (g : b₁ ⟶ b₂) →
                        map (CategoryTheory.CategoryStruct.comp f g) ≅
                          CategoryTheory.CategoryStruct.comp (map f) (map g)) →
                autoParam
                    (∀ {b₀ b₁ b₂ b₃ : B₀} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
                      CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom
                          (CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.Bicategory.whiskerRight (mapComp f g).hom (map h))
                            (CategoryTheory.CategoryStruct.comp
                              (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom
                              (CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h).inv)
                                (mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv))) =
                        CategoryTheory.eqToHom ⋯)
                    CategoryTheory.LocallyDiscrete.mkPseudofunctor._auto_1 →
                  autoParam
                      (∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁),
                        CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f).hom
                            (CategoryTheory.CategoryStruct.comp
                              (CategoryTheory.Bicategory.whiskerRight (mapId b₀).hom (map f))
                              (CategoryTheory.Bicategory.leftUnitor (map f)).hom) =
                          CategoryTheory.eqToHom ⋯)
                      CategoryTheory.LocallyDiscrete.mkPseudofunctor._auto_3 →
                    autoParam
                        (∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁),
                          CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁)).hom
                              (CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁).hom)
                                (CategoryTheory.Bicategory.rightUnitor (map f)).hom) =
                            CategoryTheory.eqToHom ⋯)
                        CategoryTheory.LocallyDiscrete.mkPseudofunctor._auto_5 →
                      CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete B₀) C
-- Mathlib.Data.Real.ConjExponents
ENNReal.HolderConjugate.conjExponent_eq : ∀ {p q : ENNReal} [h : p.HolderConjugate q], p.conjExponent = q
-- Mathlib.Geometry.Manifold.VectorBundle.Hom
/-- Consider a `C^n` map `v : M → E₁` to a vector bundle, over a base map `b : M → B`, and
linear maps `ϕ m : E₁ (b m) → E₂ (b m)` depending smoothly on `m`.
One can apply `ϕ m` to `v m`, and the resulting map is `C^n`.

We give here a version of this statement at a point.  -/
ContMDiffAt.clm_bundle_apply : ∀ {𝕜 : Type u_1} {B : Type u_2} {F₁ : Type u_3} {F₂ : Type u_4} {M : Type u_6} [inst : NontriviallyNormedField 𝕜]
  {n : WithTop ℕ∞} {E₁ : B → Type u_7} [inst_1 : (x : B) → AddCommGroup (E₁ x)] [inst_2 : (x : B) → Module 𝕜 (E₁ x)]
  [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁] [inst_5 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
  [inst_6 : (x : B) → TopologicalSpace (E₁ x)] {E₂ : B → Type u_8} [inst_7 : (x : B) → AddCommGroup (E₂ x)]
  [inst_8 : (x : B) → Module 𝕜 (E₂ x)] [inst_9 : NormedAddCommGroup F₂] [inst_10 : NormedSpace 𝕜 F₂]
  [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [inst_12 : (x : B) → TopologicalSpace (E₂ x)] {EB : Type u_10}
  [inst_13 : NormedAddCommGroup EB] [inst_14 : NormedSpace 𝕜 EB] {HB : Type u_11} [inst_15 : TopologicalSpace HB]
  {IB : ModelWithCorners 𝕜 EB HB} [inst_16 : TopologicalSpace B] [inst_17 : ChartedSpace HB B] {EM : Type u_12}
  [inst_18 : NormedAddCommGroup EM] [inst_19 : NormedSpace 𝕜 EM] {HM : Type u_13} [inst_20 : TopologicalSpace HM]
  {IM : ModelWithCorners 𝕜 EM HM} [inst_21 : TopologicalSpace M] [inst_22 : ChartedSpace HM M]
  [inst_23 : FiberBundle F₁ E₁] [inst_24 : VectorBundle 𝕜 F₁ E₁] [inst_25 : FiberBundle F₂ E₂]
  [inst_26 : VectorBundle 𝕜 F₂ E₂] {b : M → B} {v : (x : M) → E₁ (b x)} {x : M}
  [inst_27 : ∀ (x : B), IsTopologicalAddGroup (E₂ x)] [inst_28 : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
  {ϕ : (x : M) → E₁ (b x) →L[𝕜] E₂ (b x)},
  ContMDiffAt IM (IB.prod (modelWithCornersSelf 𝕜 ⋯)) n (fun m => ⟨b m, ϕ m⟩) x →
    ContMDiffAt IM (IB.prod (modelWithCornersSelf 𝕜 F₁)) n (fun m => ⟨b m, v m⟩) x →
      ContMDiffAt IM (IB.prod (modelWithCornersSelf 𝕜 F₂)) n (fun m => ⋯) x
-- Batteries.Data.FloatArray
/-- Unsafe optimized implementation of `mapM`.

This function is unsafe because it relies on the implementation limit that the size of an array is
always less than `USize.size`.
 -/
FloatArray.mapMUnsafe : {m : Type → Type u_1} → [Monad m] → FloatArray → (Float → m Float) → m FloatArray
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.any_toList : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [LawfulHashable α] [EquivBEq α]
  {p : α → Bool}, m.WF → m.toList.any p = m.any p
-- Mathlib.Tactic.Algebra.Basic
Mathlib.Tactic.Algebra.Int.cast_eq_algebraMap : ∀ (A : Type u_1) [inst : CommRing A] (n : ℤ), ↑n = (algebraMap ℤ A) n
-- Mathlib.Topology.Category.Sequential
Sequential.homeoOfIso_symm_apply : ∀ {X Y : Sequential} (f : X ≅ Y) (a : ↑Y.toTop),
  (Sequential.homeoOfIso f).symm a = (CategoryTheory.ConcreteCategory.hom f.inv) a
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.SavedState.mk.sizeOf_spec : ∀ (term : Lean.Elab.Term.SavedState) (tactic : Lean.Elab.Tactic.Grind.State),
  sizeOf { term := term, tactic := tactic } = 1 + sizeOf term + sizeOf tactic
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.contract_delete_sdiff : ∀ {α : Type u_1} (M : Matroid α) (C D : Set α), (M.contract C).delete D = (M.contract C).delete (D \ C)
-- Mathlib.Tactic.Sat.FromLRAT
Sat.Fmla.reify.prop : ∀ {v : Sat.Valuation} {f : Sat.Fmla} {p : Prop}, Sat.Fmla.reify v f p → ¬v.satisfies_fmla f → p
-- Lean.Parser.Tactic
Lean.Parser.Tactic.matchRhs.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.NormalizedHom.brecOn.go : {motive : Mathlib.Tactic.BicategoryLike.NormalizedHom → Sort u} →
  (t : Mathlib.Tactic.BicategoryLike.NormalizedHom) →
    ((t : Mathlib.Tactic.BicategoryLike.NormalizedHom) →
        Mathlib.Tactic.BicategoryLike.NormalizedHom.below t → motive t) →
      motive t ×' Mathlib.Tactic.BicategoryLike.NormalizedHom.below t
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
/-- The `X`-coordinate of a representative of `P + Q` for two distinct projective point
representatives `P` and `Q` on a Weierstrass curve.

If the representatives of `P` and `Q` are equal, then this returns the value `0`.  -/
WeierstrassCurve.Projective.addX : {R : Type r} → [CommRing R] → WeierstrassCurve.Projective R → (Fin 3 → R) → (Fin 3 → R) → R
-- Lean.Elab.Binders
Lean.Elab.Term.mkLetIdDeclView : Lean.Syntax → Lean.Elab.Term.LetIdDeclView
-- Init.Data.Vector.Lemmas
Vector.mem_push_self : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {x : α}, x ∈ xs.push x
-- Mathlib.Order.SetNotation
InfSet.mk : {α : Type u_1} → (Set α → α) → InfSet α
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.opow_one : ∀ (a : Ordinal.{u_1}), a ^ 1 = a
-- Mathlib.LinearAlgebra.Matrix.Symmetric
Matrix.IsSymm.submatrix : ∀ {α : Type u_1} {n : Type u_3} {m : Type u_4} {A : Matrix n n α}, A.IsSymm → ∀ (f : m → n), (A.submatrix f f).IsSymm
-- Aesop.ElabM
Aesop.ElabM.Context : Type
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.quasiIsoAt_π : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] (n q : ℤ),
  q < n → QuasiIsoAt (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.π✝ f n) q
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.nontrivial_iff : ∀ {G : Type u_1} [inst : AddGroup G], Nontrivial (AddSubgroup G) ↔ Nontrivial G
-- Mathlib.Topology.Order.Compact
cocompact_le_atTop : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderBot α] [CompactIccSpace α],
  Filter.cocompact α ≤ Filter.atTop
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.topEquiv_symm_apply_coe : ∀ {R : Type u} [inst : NonAssocSemiring R] (r : R), ↑(Subsemiring.topEquiv.symm r) = r
-- Lean.Meta.Tactic.Grind.Types
/-- Opaque solver extension state.  -/
Lean.Meta.Grind.SolverExtensionStateSpec : (α : Type) × Inhabited α
-- Lean.Meta.Basic
Lean.Meta.modifyDiag : (Lean.Meta.Diagnostics → Lean.Meta.Diagnostics) → Lean.MetaM Unit
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.inter_vadd_union_subset_union : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {s₁ s₂ : Set α} {t₁ t₂ : Set β},
  s₁ ∩ s₂ +ᵥ t₁ ∪ t₂ ⊆ (s₁ +ᵥ t₁) ∪ (s₂ +ᵥ t₂)
-- Init.Data.Vector.Monadic
Vector.foldrM_attachWith : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {xs : Vector α n}
  {q : α → Prop} (H : ∀ a ∈ xs, q a) {f : { x // q x } → β → m β} {b : β},
  Vector.foldrM f b (xs.attachWith q H) = Vector.foldrM (fun a acc => f ⟨↑a, ⋯⟩ acc) b xs.attach
-- Mathlib.Data.Num.ZNum
_private.Mathlib.Data.Num.ZNum.0.ZNum.ofInt'.match_1.eq_2 : ∀ (motive : ℤ → Sort u_1) (n : ℕ) (h_1 : (n : ℕ) → motive (Int.ofNat n)) (h_2 : (n : ℕ) → motive (Int.negSucc n)),
  (match Int.negSucc n with
    | Int.ofNat n => h_1 n
    | Int.negSucc n => h_2 n) =
    h_2 n
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.coe_insert : ∀ (x y : ZFSet.{u_1}), ↑(insert x y) = insert x ↑y
-- Init.Data.Option.Lemmas
Option.isSome_ite' : ∀ {α : Type u_1} {b : α} {p : Prop} {x : Decidable p}, (if p then none else some b).isSome = true ↔ ¬p
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.max?.match_1.eq_3 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (c : RBTree.RBColor) (l : RBTree.RBNode α) (v : α)
  (r : RBTree.RBNode α) (h_1 : Unit → motive RBTree.RBNode.nil)
  (h_2 : (c : RBTree.RBColor) → (l : RBTree.RBNode α) → (v : α) → motive (RBTree.RBNode.node c l v RBTree.RBNode.nil))
  (h_3 :
    (c : RBTree.RBColor) →
      (l : RBTree.RBNode α) → (v : α) → (r : RBTree.RBNode α) → motive (RBTree.RBNode.node c l v r)),
  (r = RBTree.RBNode.nil → False) →
    (match RBTree.RBNode.node c l v r with
      | RBTree.RBNode.nil => h_1 ()
      | RBTree.RBNode.node c l v RBTree.RBNode.nil => h_2 c l v
      | RBTree.RBNode.node c l v r => h_3 c l v r) =
      h_3 c l v r
-- Mathlib.InformationTheory.Hamming
hammingDist_smul_le_hammingDist : ∀ {α : Type u_1} {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)]
  [inst_2 : (i : ι) → SMul α (β i)] {k : α} {x y : (i : ι) → β i}, hammingDist (k • x) (k • y) ≤ hammingDist x y
-- Mathlib.Tactic.ENatToNat
Mathlib.Tactic.ENatToNat.coe_mul : ∀ (m n : ℕ), ↑m * ↑n = ↑(m * n)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings
PresheafOfModules.instFullRestrictScalarsIdFunctorOppositeRingCat : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat},
  (PresheafOfModules.restrictScalars (CategoryTheory.CategoryStruct.id R)).Full
-- Mathlib.GroupTheory.Sylow
Subgroup.sylow_mem_fixedPoints_iff : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] (H : Subgroup G) {P : Sylow p G},
  P ∈ MulAction.fixedPoints (↥H) (Sylow p G) ↔ H ≤ Subgroup.normalizer ↑P
-- Mathlib.Analysis.Calculus.DifferentialForm.Basic
/-- The second exterior derivative of a sufficiently smooth differential form is zero.  -/
extDeriv_extDeriv : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ} {r : WithTop ℕ∞}
  {ω : E → E [⋀^Fin n]→L[𝕜] F}, ContDiff 𝕜 r ω → minSmoothness 𝕜 2 ≤ r → extDeriv (extDeriv ω) = 0
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
ENNReal.instMeasurableInv : MeasurableInv ENNReal
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.map_obj : ∀ {X Y : TopCat} (f : X ⟶ Y) (U : Set ↑Y) (p : IsOpen U),
  (TopologicalSpace.Opens.map f).obj { carrier := U, is_open' := p } =
    { carrier := ⇑(CategoryTheory.ConcreteCategory.hom f) ⁻¹' U, is_open' := ⋯ }
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.postcomp_obj : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {b c : B} (a : B) (f : b ⟶ c) (x : a ⟶ b),
  (CategoryTheory.Bicategory.postcomp a f).obj x = CategoryTheory.CategoryStruct.comp x f
-- Mathlib.Order.SuccPred.Limit
Order.isPredPrelimit_iff_of_noMin : ∀ {α : Type u_1} {a : α} [inst : Preorder α] [inst_1 : PredOrder α] [IsPredArchimedean α] [NoMinOrder α],
  Order.IsPredPrelimit a ↔ IsMax a
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.unop_prod : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] (s : Finset ι) (f : ι → Mᵐᵒᵖ),
  AddOpposite.unop (∏ i ∈ s, f i) = ∏ i ∈ s, AddOpposite.unop (f i)
-- Init.Data.List.Basic
List.erase_nil : ∀ {α : Type u} [inst : BEq α] (a : α), [].erase a = []
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.BindStruct.fac : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Presieve X}
  {R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → CategoryTheory.Presieve Y} {Z : C} {h : Z ⟶ X} (self : S.BindStruct R h),
  CategoryTheory.CategoryStruct.comp self.g self.f = h
-- Mathlib.CategoryTheory.Sites.GlobalSections
/-- Naturality lemma for `ΓHomEquiv` analogous to `Adjunction.homEquiv_naturality_left`.  -/
CategoryTheory.Sheaf.ΓHomEquiv_naturality_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} A] [inst_2 : CategoryTheory.HasWeakSheafify J A]
  [inst_3 : CategoryTheory.HasGlobalSectionsFunctor J A] {X' X : A} {F : CategoryTheory.Sheaf J A} (f : X' ⟶ X)
  (g : (CategoryTheory.Functor.const Cᵒᵖ).obj X ⟶ F.obj),
  CategoryTheory.Sheaf.ΓHomEquiv (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.const Cᵒᵖ).map f) g) =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.Sheaf.ΓHomEquiv g)
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.instInfSet : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : AddCommGroup M] → [inst_3 : Module R M] → [inst_4 : LieRingModule L M] → InfSet (LieSubmodule R L M)
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.fillNones.match_1.eq_4 : ∀ {α : Type u_1} (motive : List (Option α) → List α → Sort u_2) (as : List (Option α)) (a : α) (as' : List α)
  (h_1 : (x : List α) → motive [] x)
  (h_2 : (a : α) → (as : List (Option α)) → (as' : List α) → motive (some a :: as) as')
  (h_3 : (as : List (Option α)) → motive (none :: as) [])
  (h_4 : (as : List (Option α)) → (a : α) → (as' : List α) → motive (none :: as) (a :: as')),
  (match none :: as, a :: as' with
    | [], x => h_1 x
    | some a :: as, as' => h_2 a as as'
    | none :: as, [] => h_3 as
    | none :: as, a :: as' => h_4 as a as') =
    h_4 as a as'
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.comp_id : ∀ {E : Type u_3} [inst : AddGroup E] (p : AddGroupSeminorm E), p.comp (AddMonoidHom.id E) = p
-- Mathlib.RingTheory.EuclideanDomain
left_div_gcd_ne_zero : ∀ {R : Type u_1} [inst : EuclideanDomain R] [inst_1 : GCDMonoid R] {p q : R}, p ≠ 0 → p / gcd p q ≠ 0
-- Mathlib.Analysis.Normed.Operator.Prod
Continuous.prod_map_equivL : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {M₁ : Type u_5} {M₂ : Type u_6} {M₃ : Type u_7} {M₄ : Type u_8}
  [inst_1 : SeminormedAddCommGroup M₁] [inst_2 : NormedSpace 𝕜 M₁] [inst_3 : SeminormedAddCommGroup M₂]
  [inst_4 : NormedSpace 𝕜 M₂] [inst_5 : SeminormedAddCommGroup M₃] [inst_6 : NormedSpace 𝕜 M₃]
  [inst_7 : SeminormedAddCommGroup M₄] [inst_8 : NormedSpace 𝕜 M₄] {X : Type u_9} [inst_9 : TopologicalSpace X]
  {f : X → M₁ ≃L[𝕜] M₂} {g : X → M₃ ≃L[𝕜] M₄},
  (Continuous fun x => ↑(f x)) → (Continuous fun x => ↑(g x)) → Continuous fun x => ↑((f x).prodCongr (g x))
-- Lean.Declaration
Lean.Declaration.defnDecl.inj : ∀ {val val_1 : Lean.DefinitionVal}, Lean.Declaration.defnDecl val = Lean.Declaration.defnDecl val_1 → val = val_1
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.prodEquiv_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  {B : Type u_3} [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  {C : Type u_4} [inst_7 : Semiring C] [inst_8 : Algebra R C] [inst_9 : TopologicalSpace C]
  (f : (A →A[R] B) × (A →A[R] C)), ContinuousAlgHom.prodEquiv f = f.1.prod f.2
-- Mathlib.Analysis.Analytic.Composition
/-- Eta-expanded form of `CPolynomialAt.comp_of_eq`

---

Version of `CPolynomialAt.comp` where point equality is a separate hypothesis.  -/
CPolynomialAt.fun_comp_of_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {g : F → G} {f : E → F} {y : F} {x : E},
  CPolynomialAt 𝕜 g y → CPolynomialAt 𝕜 f x → f x = y → CPolynomialAt 𝕜 (fun x => g (f x)) x
-- Std.Data.HashMap.Raw
Std.HashMap.Raw.instInsertProdOfBEqOfHashable : {α : Type u} → {β : Type v} → [BEq α] → [Hashable α] → Insert (α × β) (Std.HashMap.Raw α β)
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Poly.insert.go.match_1.eq_3 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.eq) (h_2 : Unit → motive Ordering.gt)
  (h_3 : Unit → motive Ordering.lt),
  (match Ordering.lt with
    | Ordering.eq => h_1 ()
    | Ordering.gt => h_2 ()
    | Ordering.lt => h_3 ()) =
    h_3 ()
-- Lean.Expr
Lean.mkLetEx : Lean.Name → Lean.Expr → Lean.Expr → Lean.Expr → Bool → Lean.Expr
-- Mathlib.Combinatorics.Quiver.ReflQuiver
/-- An equality of refl prefunctors gives an equality on homs.  -/
CategoryTheory.ReflPrefunctor.congr_hom : ∀ {U : Type u_1} {V : Type u_2} [inst : CategoryTheory.ReflQuiver U] [inst_1 : CategoryTheory.ReflQuiver V]
  {F G : U ⥤rq V} (e : F = G) {X Y : U} (f : X ⟶ Y), Quiver.homOfEq (F.map f) ⋯ ⋯ = G.map f
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Initial.limitIso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : F.Initial] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  (G : CategoryTheory.Functor D E) [inst_4 : CategoryTheory.Limits.HasLimit G],
  (CategoryTheory.Functor.Initial.limitIso F G).hom = CategoryTheory.inv (CategoryTheory.Limits.limit.pre G F)
-- Mathlib.Analysis.Analytic.IteratedFDeriv
/-- If a function has a power series in a ball, then its `n`-th iterated derivative is given by
`(v₁, ..., vₙ) ↦ ∑ pₙ (v_{σ (1)}, ..., v_{σ (n)})` where the sum is over all
permutations of `{1, ..., n}`.  -/
HasFPowerSeriesOnBall.iteratedFDeriv_eq_sum_of_completeSpace : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} [CompleteSpace F],
  HasFPowerSeriesOnBall f p x r → ∀ {n : ℕ} (v : Fin n → E), (iteratedFDeriv 𝕜 n f x) v = ∑ σ, (p n) fun i => v (σ i)
-- Mathlib.AlgebraicGeometry.Morphisms.Finite
/-- A morphism of schemes `X ⟶ Y` is finite if
the preimage of any affine open subset of `Y` is affine and the induced ring
hom is finite.  -/
AlgebraicGeometry.IsFinite : {X Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → Prop
-- Mathlib.Algebra.Ring.Subring.MulOpposite
Subring.unop_iInf : ∀ {ι : Sort u_1} {R : Type u_2} [inst : NonAssocRing R] (S : ι → Subring Rᵐᵒᵖ), (iInf S).unop = ⨅ i, (S i).unop
-- Lean.Elab.PreDefinition.Structural.FindRecArg
/-- Reorders the `RecArgInfos` of one function to put arguments that are indices of other arguments
last.
See issue #837 for an example where we can show termination using the index of an inductive family, but
we don't get the desired definitional equalities.
 -/
Lean.Elab.Structural.nonIndicesFirst : Array Lean.Elab.Structural.RecArgInfo → Array Lean.Elab.Structural.RecArgInfo
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
/-- A `2`-pretransitive additive action is pretransitive.  -/
AddAction.isPretransitive_of_is_two_pretransitive : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α]
  [h2 : AddAction.IsMultiplyPretransitive G α 2], AddAction.IsPretransitive G α
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
extChartAt_prod : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} {E' : Type u_5} {M' : Type u_6} {H' : Type u_7}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M] {I : ModelWithCorners 𝕜 E H}
  [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E'] [inst_7 : TopologicalSpace H']
  [inst_8 : TopologicalSpace M'] {I' : ModelWithCorners 𝕜 E' H'} [inst_9 : ChartedSpace H M]
  [inst_10 : ChartedSpace H' M'] (x : M × M'), extChartAt (I.prod I') x = (extChartAt I x.1).prod (extChartAt I' x.2)
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousLinearMap.compContinuousAlternatingMap_coe : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {N' : Type u_5} {ι : Type u_6} [inst : Semiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N]
  [inst_5 : Module R N] [inst_6 : TopologicalSpace N] [inst_7 : AddCommMonoid N'] [inst_8 : Module R N']
  [inst_9 : TopologicalSpace N'] (g : N →L[R] N') (f : M [⋀^ι]→L[R] N), ⇑(g.compContinuousAlternatingMap f) = ⇑g ∘ ⇑f
-- Lean.Compiler.Specialize
Lean.Compiler.SpecializeAttributeKind : Type
-- Mathlib.FieldTheory.Perfect
RingHom.map_iterate_frobeniusEquiv_symm : ∀ {R : Type u_2} {S : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring S] (p : ℕ) [inst_2 : ExpChar R p]
  [inst_3 : PerfectRing R p] [inst_4 : ExpChar S p] [inst_5 : PerfectRing S p] (f : R →+* S) (n : ℕ) (x : R),
  f ((⇑(frobeniusEquiv R p).symm)^[n] x) = (⇑(frobeniusEquiv S p).symm)^[n] (f x)
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
csSup_Ioo : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {a b : α} [DenselyOrdered α], a < b → sSup (Set.Ioo a b) = b
-- Mathlib.Data.Multiset.Filter
Multiset.map_filterMap_of_inv : ∀ {α : Type u_1} {β : Type v} (f : α → Option β) (g : β → α),
  (∀ (x : α), Option.map g (f x) = some x) → ∀ (s : Multiset α), Multiset.map g (Multiset.filterMap f s) = s
-- Mathlib.FieldTheory.Galois.Abelian
IsAbelianGalois.of_isCyclic : ∀ (K : Type u_1) (L : Type u_2) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [IsGalois K L]
  [IsCyclic Gal(L/K)], IsAbelianGalois K L
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.NumDenSameDeg.den_pow : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubmonoidClass σ A] {𝒜 : ι → σ} (x : Submonoid A) [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι]
  [inst_5 : GradedRing 𝒜] (c : HomogeneousLocalization.NumDenSameDeg 𝒜 x) (n : ℕ), ↑(c ^ n).den = ↑c.den ^ n