mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered
/-- More precise variant of the lemma `ιColimitType_eq_iff_of_isFiltered`
in the case both `x` and `y` are in the same type `F.obj j`.  -/
CategoryTheory.Functor.ιColimitType_eq_iff_of_isFiltered' : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] [CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J (Type w₀)) {j : J} (x y : F.obj j),
  F.ιColimitType j x = F.ιColimitType j y ↔
    ∃ k f, (CategoryTheory.ConcreteCategory.hom (F.map f)) x = (CategoryTheory.ConcreteCategory.hom (F.map f)) y
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.isLittleOTVS_pi : ∀ {α : Type u_1} {𝕜 : Type u_3} {F : Type u_5} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup F]
  [inst_2 : TopologicalSpace F] [inst_3 : Module 𝕜 F] {l : Filter α} {g : α → F} {ι : Type u_7} {E : ι → Type u_8}
  [inst_4 : (i : ι) → AddCommGroup (E i)] [inst_5 : (i : ι) → Module 𝕜 (E i)]
  [inst_6 : (i : ι) → TopologicalSpace (E i)] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] {f : α → (i : ι) → E i},
  f =o[𝕜; l] g ↔ ∀ (i : ι), (fun x => f x i) =o[𝕜; l] g
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey!_insertListIfNewUnit_of_contains_eq_false_of_mem : ∀ {α : Type u} [inst : BEq α] [EquivBEq α] [inst_2 : Inhabited α] {l : List ((_ : α) × Unit)} {toInsert : List α}
  {k k' : α},
  (k == k') = true →
    Std.Internal.List.containsKey k l = false →
      List.Pairwise (fun a b => (a == b) = false) toInsert →
        k ∈ toInsert → Std.Internal.List.getKey! k' (Std.Internal.List.insertListIfNewUnit l toInsert) = k
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution'.ha : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3}
  (self : FermatLastTheoremForThreeGen.Solution'✝ hζ),
  ¬hζ.toInteger - 1 ∣ FermatLastTheoremForThreeGen.Solution'.a✝ self
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.log_one : Real.log 1 = 0
-- Mathlib.Algebra.MvPolynomial.Derivation
MvPolynomial.derivation_ext : ∀ {σ : Type u_1} {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Module (MvPolynomial σ R) A] {D₁ D₂ : Derivation R (MvPolynomial σ R) A},
  (∀ (i : σ), D₁ (MvPolynomial.X i) = D₂ (MvPolynomial.X i)) → D₁ = D₂
-- Mathlib.Algebra.QuadraticAlgebra.Basic
/-- the norm in a quadratic algebra, as a `MonoidHom`.  -/
QuadraticAlgebra.norm : {R : Type u_2} → {a b : R} → [inst : CommRing R] → QuadraticAlgebra R a b →* R
-- Mathlib.Data.Finsupp.Basic
/-- `frange f` is the image of `f` on the support of `f`.  -/
Finsupp.frange : {α : Type u_1} → {M : Type u_5} → [inst : Zero M] → (α →₀ M) → Finset M
-- Mathlib.Order.Defs.PartialOrder
/-- `WCovBy a b` means that `a = b` or `b` covers `a`.
This means that `a ≤ b` and there is no element in between. This is denoted `a ⩿ b`.
 -/
WCovBy : {α : Type u_1} → [Preorder α] → α → α → Prop
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas
RootPairing.chainBotCoeff_mul_chainTopCoeff.isNotG2 : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [CharZero R] [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} [Finite ι] [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.IsNotG2
-- Mathlib.Topology.Algebra.UniformConvergence
instSubUniformOnFun : {α : Type u_1} → {β : Type u_2} → {𝔖 : Set (Set α)} → [Sub β] → Sub (UniformOnFun α β 𝔖)
-- Mathlib.Combinatorics.Nullstellensatz
/-- The polynomial in `X i` that vanishes at all elements of `S`.  -/
_private.Mathlib.Combinatorics.Nullstellensatz.0.MvPolynomial.Alon.P : {R : Type u_1} → [inst : CommRing R] → {σ : Type u_2} → Finset R → σ → MvPolynomial σ R
-- Mathlib.LinearAlgebra.Matrix.Symmetric
Matrix.IsSymm.sub : ∀ {α : Type u_1} {n : Type u_3} {A B : Matrix n n α} [inst : Sub α], A.IsSymm → B.IsSymm → (A - B).IsSymm
-- Mathlib.Data.Set.Equitable
Set.equitableOn_iff_exists_le_le_add_one : ∀ {α : Type u_1} {s : Set α} {f : α → ℕ}, s.EquitableOn f ↔ ∃ b, ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1
-- Mathlib.AlgebraicTopology.SimplexCategory.Truncated
SimplexCategory.Truncated.δ₂_zero_comp_δ₂_two_assoc : ∀ {Z : CategoryTheory.ObjectProperty.FullSubcategory fun a => a.len ≤ 2}
  (h : { obj := { len := 0 + 1 + 1 }, property := SimplexCategory.Truncated.δ₂_zero_comp_δ₂_two._proof_1 } ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (SimplexCategory.Truncated.δ₂ 0 SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_4
        SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_3)
      (CategoryTheory.CategoryStruct.comp
        (SimplexCategory.Truncated.δ₂ 2 SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_3
          SimplexCategory.Truncated.δ₂_zero_comp_δ₂_two._proof_1)
        h) =
    CategoryTheory.CategoryStruct.comp
      (SimplexCategory.Truncated.δ₂ 1 SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_4
        SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_3)
      (CategoryTheory.CategoryStruct.comp
        (SimplexCategory.Truncated.δ₂ 0 SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_3
          SimplexCategory.Truncated.δ₂_zero_comp_δ₂_two._proof_1)
        h)
-- Lean.Elab.Tactic.ElabTerm
Lean.Elab.Tactic.evalConstructor : Lean.Elab.Tactic.Tactic
-- Lean.Compiler.NameMangling
_private.Lean.Compiler.NameMangling.0.String.pushHex.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (k : ℕ) (h_1 : Unit → motive 0) (h_2 : (k : ℕ) → motive k.succ),
  (match k.succ with
    | 0 => h_1 ()
    | k.succ => h_2 k) =
    h_2 k
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
/-- The identity map of fixing additive subgroup of stabilizer
into the fixing additive subgroup of the extended set, as an equivariant map.  -/
SubAddAction.ofFixingAddSubgroup_insert_map : {M : Type u_1} →
  {α : Type u_2} →
    [inst : AddGroup M] →
      [inst_1 : AddAction M α] →
        (a : α) →
          (s : Set ↥(SubAddAction.ofStabilizer M a)) →
            ↥(SubAddAction.ofFixingAddSubgroup M
                  (insert a (Subtype.val '' s))) →ₑ[⇑(SubAddAction.fixingAddSubgroupInsertEquiv a s)]
              ↥(SubAddAction.ofFixingAddSubgroup (↥(AddAction.stabilizer M a)) s)
-- Mathlib.Data.DFinsupp.NeLocus
DFinsupp.neLocus_sub_right : ∀ {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] [inst_1 : (a : α) → DecidableEq (N a)]
  [inst_2 : (a : α) → AddGroup (N a)] (f₁ f₂ g : Π₀ (a : α), N a), (f₁ - g).neLocus (f₂ - g) = f₁.neLocus f₂
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBiconeMorphism.mk.injEq : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} {A B : CategoryTheory.Limits.BinaryBicone P Q} (hom : A.pt ⟶ B.pt)
  (wfst :
    autoParam (CategoryTheory.CategoryStruct.comp hom B.fst = A.fst)
      CategoryTheory.Limits.BinaryBiconeMorphism.wfst._autoParam)
  (wsnd :
    autoParam (CategoryTheory.CategoryStruct.comp hom B.snd = A.snd)
      CategoryTheory.Limits.BinaryBiconeMorphism.wsnd._autoParam)
  (winl :
    autoParam (CategoryTheory.CategoryStruct.comp A.inl hom = B.inl)
      CategoryTheory.Limits.BinaryBiconeMorphism.winl._autoParam)
  (winr :
    autoParam (CategoryTheory.CategoryStruct.comp A.inr hom = B.inr)
      CategoryTheory.Limits.BinaryBiconeMorphism.winr._autoParam)
  (hom_1 : A.pt ⟶ B.pt)
  (wfst_1 :
    autoParam (CategoryTheory.CategoryStruct.comp hom_1 B.fst = A.fst)
      CategoryTheory.Limits.BinaryBiconeMorphism.wfst._autoParam)
  (wsnd_1 :
    autoParam (CategoryTheory.CategoryStruct.comp hom_1 B.snd = A.snd)
      CategoryTheory.Limits.BinaryBiconeMorphism.wsnd._autoParam)
  (winl_1 :
    autoParam (CategoryTheory.CategoryStruct.comp A.inl hom_1 = B.inl)
      CategoryTheory.Limits.BinaryBiconeMorphism.winl._autoParam)
  (winr_1 :
    autoParam (CategoryTheory.CategoryStruct.comp A.inr hom_1 = B.inr)
      CategoryTheory.Limits.BinaryBiconeMorphism.winr._autoParam),
  ({ hom := hom, wfst := wfst, wsnd := wsnd, winl := winl, winr := winr } =
      { hom := hom_1, wfst := wfst_1, wsnd := wsnd_1, winl := winl_1, winr := winr_1 }) =
    (hom = hom_1)
-- Mathlib.Order.Hom.Lattice
SupHom.dual_apply_toFun : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : Max β] (f : SupHom α β) (a : α), (SupHom.dual f) a = f a
-- Mathlib.LinearAlgebra.Complex.Module
imaginaryPart_comp_subtype_selfAdjoint : ∀ {A : Type u_1} [inst : AddCommGroup A] [inst_1 : Module ℂ A] [inst_2 : StarAddMonoid A] [inst_3 : StarModule ℂ A],
  imaginaryPart ∘ₗ (selfAdjoint.submodule ℝ A).subtype = 0
-- Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
tendsto_rpow_atBot_of_base_lt_one : ∀ (b : ℝ), 0 < b → b < 1 → Filter.Tendsto (fun x => b ^ x) Filter.atBot Filter.atTop
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.LeftExtension.precomp₂_obj_left : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] {F₀ : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  {F₁ : CategoryTheory.Functor D H} (L' : CategoryTheory.Functor D D') (α : F₀ ⟶ L.comp F₁) (X : L'.LeftExtension F₁),
  ((CategoryTheory.Functor.LeftExtension.precomp₂ L' α).obj X).left = X.left
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.lift_apply_inl : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : Monoid P]
  (f : M →* P) (g : N →* P) (x : M), (Monoid.Coprod.lift f g) (Monoid.Coprod.inl x) = f x
-- Mathlib.Logic.Encodable.Basic
Encodable.encode_star : Encodable.encode PUnit.unit = 0
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.LawfulToForwardSearcherModel.defaultImplementation : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat]
  [inst_1 : String.Slice.Pattern.StrictForwardPattern pat] [inst_2 : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.LawfulForwardPatternModel pat],
  String.Slice.Pattern.Model.LawfulToForwardSearcherModel pat
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
AddMonCat.FilteredColimits.colimitAdd.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCat)
  [inst_1 : CategoryTheory.IsFiltered J],
  AddMonCat.FilteredColimits.colimitAdd F =
    { add := fun x y => Quot.lift₂ (AddMonCat.FilteredColimits.colimitAddAux F) ⋯ ⋯ x y }
-- Mathlib.Data.Set.UnionLift
Set.preimage_liftCover : ∀ {α : Type u_1} {ι : Sort u_3} {β : Type u_2} {S : ι → Set α} {f : (i : ι) → ↑(S i) → β}
  {hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩} {hS : Set.iUnion S = Set.univ}
  (t : Set β), Set.liftCover S f hf hS ⁻¹' t = ⋃ i, Subtype.val '' f i ⁻¹' t
-- Mathlib.Probability.Kernel.Composition.Comp
ProbabilityTheory.Kernel.comp_apply_univ_le : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel β γ) (a : α),
  ((η.comp κ) a) Set.univ ≤ (κ a) Set.univ * η.bound
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.leadingTerm_monomial : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] (s : σ →₀ ℕ) (c : R),
  m.leadingTerm ((MvPolynomial.monomial s) c) = (MvPolynomial.monomial s) c
-- Init.Data.Nat.Control
_private.Init.Data.Nat.Control.0.Nat.foldRevM.loop : {α : Type u} → {m : Type u → Type v} → [Monad m] → (n : ℕ) → ((i : ℕ) → i < n → α → m α) → (i : ℕ) → i ≤ n → α → m α
-- Mathlib.AlgebraicGeometry.Morphisms.Etale
AlgebraicGeometry.Etale.instResLE : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : X.Opens) (V : Y.Opens)
  (e : U ≤ (TopologicalSpace.Opens.map f.base).obj V) [AlgebraicGeometry.Etale f],
  AlgebraicGeometry.Etale (AlgebraicGeometry.Scheme.Hom.resLE f V U e)
-- Mathlib.Data.Vector.Basic
/-- The natural equivalence between length-`n` vectors and functions from `Fin n`.  -/
Equiv.vectorEquivFin : (α : Type u_6) → (n : ℕ) → List.Vector α n ≃ (Fin n → α)
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.fst_pow : ∀ {α : Type u_2} [inst : Monoid α] [inst_1 : Preorder α] [inst_2 : MulLeftMono α] [inst_3 : MulRightMono α]
  (s : NonemptyInterval α) (n : ℕ), (s ^ n).toProd.1 = s.toProd.1 ^ n
-- Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian
CategoryTheory.Idempotents.DoldKan.N_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.IsIdempotentComplete C] [inst_3 : CategoryTheory.Limits.HasFiniteCoproducts C]
  (X : CategoryTheory.SimplicialObject C),
  CategoryTheory.Idempotents.DoldKan.N.obj X =
    (CategoryTheory.Idempotents.toKaroubiEquivalence (ChainComplex C ℕ)).inverse.obj
      (AlgebraicTopology.DoldKan.N₁.obj X)
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.addLeft_toEquiv : ∀ {G : Type v} [inst : AddGroup G] [inst_1 : PseudoEMetricSpace G] [inst_2 : IsIsometricVAdd G G] (c : G),
  (IsometryEquiv.addLeft c).toEquiv = Equiv.addLeft c
-- Mathlib.NumberTheory.LSeries.Nonvanishing
_private.Mathlib.NumberTheory.LSeries.Nonvanishing.0.DirichletCharacter.BadChar.F.eq_1 : ∀ {N : ℕ} [inst : NeZero N] (B : DirichletCharacter.BadChar✝ N),
  DirichletCharacter.BadChar.F✝ B =
    Function.update (fun s => riemannZeta s * DirichletCharacter.LFunction (DirichletCharacter.BadChar.χ✝ B) s) 1
      (deriv (DirichletCharacter.LFunction (DirichletCharacter.BadChar.χ✝ B)) 1)
-- Mathlib.Analysis.Fourier.ZMod
ZMod.dft_comp_neg : ∀ {N : ℕ} [inst : NeZero N] {E : Type u_1} [inst_1 : AddCommGroup E] [inst_2 : Module ℂ E] (Φ : ZMod N → E),
  (ZMod.dft fun j => Φ (-j)) = fun k => ZMod.dft Φ (-k)
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.GrothendieckTopology.Point.instPreservesFiniteLimitsSheafSheafFiberOfLocallySmallOfHasFiniteLimitsOfAB5OfSize : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C]
  [CategoryTheory.Limits.HasFiniteLimits A] [CategoryTheory.AB5OfSize.{w, w, v', u'} A],
  CategoryTheory.Limits.PreservesFiniteLimits Φ.sheafFiber
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.getEntryLT! : {α : Type u} →
  {β : α → Type v} → [Ord α] → [Inhabited ((a : α) × β a)] → α → Std.DTreeMap.Internal.Impl α β → (a : α) × β a
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.bsup_lt_ord : ∀ {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{u}} {c : Ordinal.{u}},
  o.card < c.cof → (∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c) → o.bsup f < c
-- Mathlib.Order.RelClasses
/-- Derive a `WellFoundedRelation` instance from a `WellFoundedLT` instance.  -/
WellFoundedLT.toWellFoundedRelation : {α : Type u} → [inst : LT α] → [WellFoundedLT α] → WellFoundedRelation α
-- Lean.Data.PersistentArray
Lean.PersistentArrayNode.brecOn_2.eq : ∀ {α : Type u} {motive_1 : Lean.PersistentArrayNode α → Sort u_1}
  {motive_2 : Array (Lean.PersistentArrayNode α) → Sort u_1} {motive_3 : List (Lean.PersistentArrayNode α) → Sort u_1}
  (t : List (Lean.PersistentArrayNode α)) (F_1 : (t : Lean.PersistentArrayNode α) → t.below → motive_1 t)
  (F_2 : (t : Array (Lean.PersistentArrayNode α)) → Lean.PersistentArrayNode.below_1 t → motive_2 t)
  (F_3 : (t : List (Lean.PersistentArrayNode α)) → Lean.PersistentArrayNode.below_2 t → motive_3 t),
  Lean.PersistentArrayNode.brecOn_2 t F_1 F_2 F_3 = F_3 t (Lean.PersistentArrayNode.brecOn_2.go t F_1 F_2 F_3).2
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.mapAlongAddMonoidHom.eq_1 : ∀ {ι₁ : Type u_3} {ι₂ : Type u_4} (R₁ : ι₁ → Type u_5) (R₂ : ι₂ → Type u_6) {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂}
  {S₁ : ι₁ → Type u_7} {S₂ : ι₂ → Type u_8} [inst : (i : ι₁) → SetLike (S₁ i) (R₁ i)]
  [inst_1 : (j : ι₂) → SetLike (S₂ j) (R₂ j)] {B₁ : (i : ι₁) → S₁ i} {B₂ : (j : ι₂) → S₂ j} (f : ι₂ → ι₁)
  (hf : Filter.Tendsto f 𝓕₂ 𝓕₁) [inst_2 : (i : ι₁) → AddMonoid (R₁ i)] [inst_3 : (i : ι₂) → AddMonoid (R₂ i)]
  [inst_4 : ∀ (i : ι₁), AddSubmonoidClass (S₁ i) (R₁ i)] [inst_5 : ∀ (i : ι₂), AddSubmonoidClass (S₂ i) (R₂ i)]
  (φ : (j : ι₂) → R₁ (f j) →+ R₂ j) (hφ : ∀ᶠ (j : ι₂) in 𝓕₂, Set.MapsTo ⇑(φ j) ↑(B₁ (f j)) ↑(B₂ j)),
  RestrictedProduct.mapAlongAddMonoidHom R₁ R₂ f hf φ hφ =
    { toFun := RestrictedProduct.mapAlong R₁ R₂ f hf (fun j r => (φ j) r) hφ, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Order.Hom.CompleteLattice
/-- An equivalence of types yields an order isomorphism between their lattices of subsets.  -/
Equiv.toOrderIsoSet : {α : Type u_2} → {β : Type u_3} → α ≃ β → Set α ≃o Set β
-- Mathlib.Order.SupClosed
lowerBounds_infClosure : ∀ {α : Type u_3} [inst : SemilatticeInf α] (s : Set α), lowerBounds (infClosure s) = lowerBounds s
-- Init.Data.Array.Erase
Array.mem_erase_of_ne : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a b : α} {xs : Array α}, a ≠ b → (a ∈ xs.erase b ↔ a ∈ xs)
-- Mathlib.FieldTheory.Finite.GaloisField
FiniteField.splits_X_pow_nat_card_sub_X : ∀ (p : ℕ) [h_prime : Fact (Nat.Prime p)] {K : Type u_1} [inst : Field K] [inst_1 : Algebra (ZMod p) K] [Finite K],
  (Polynomial.map (algebraMap (ZMod p) K) (Polynomial.X ^ Nat.card K - Polynomial.X)).Splits
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.re_zero : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : Zero R], QuaternionAlgebra.re 0 = 0
-- Mathlib.Data.List.Induction
List.bidirectionalRec_cons_append : ∀ {α : Type u_1} {motive : List α → Sort u_2} (nil : motive []) (singleton : (a : α) → motive [a])
  (cons_append : (a : α) → (l : List α) → (b : α) → motive l → motive (a :: (l ++ [b]))) (a : α) (l : List α) (b : α),
  List.bidirectionalRec nil singleton cons_append (a :: (l ++ [b])) =
    cons_append a l b (List.bidirectionalRec nil singleton cons_append l)
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
/-- Given a regular cardinal `κ` and a type `X`, this is the `κ`-filtered
partially ordered type of subsets of `X` of cardinality `< κ`,
as an object of the category `CardinalDirectedPoset κ`.  -/
CategoryTheory.CardinalDirectedPoset.setCardinalLT : (κ : Cardinal.{u}) → [inst : Fact κ.IsRegular] → Type u → CategoryTheory.CardinalDirectedPoset κ
-- Std.Do.WP.SimpLemmas
_private.Std.Do.WP.SimpLemmas.0.Std.Do.PredTrans.pushExcept.match_1.splitter : {α ε : Type u_1} →
  (motive : Except ε α → Sort u_2) →
    (x : Except ε α) → ((a : α) → motive (Except.ok a)) → ((e : ε) → motive (Except.error e)) → motive x
-- Mathlib.Data.Nat.Choose.Cast
Nat.cast_choose_two : ∀ (K : Type u_1) [inst : DivisionRing K] [NeZero 2] (a : ℕ), ↑(a.choose 2) = ↑a * (↑a - 1) / 2
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_inv_le_iff_of_pos : ∀ {z : ℝ} {y : NNReal}, 0 ≤ y → 0 < z → ∀ (x : NNReal), x ^ z⁻¹ ≤ y ↔ x ≤ y ^ z
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.eq_comp_toLinearMap_symm : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_8} {M₂ : Type u_9} {M₃ : Type u_10} [inst : Semiring R₁]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃}
  {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₁₃ : R₁ →+* R₃} {σ₂₃ : R₂ →+* R₃} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
  {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} [inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂}
  [inst_7 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃] (f : M₂ →ₛₗ[σ₂₃] M₃) (g : M₁ →ₛₗ[σ₁₃] M₃),
  f = g ∘ₛₗ ↑e₁₂.symm ↔ f ∘ₛₗ ↑e₁₂ = g
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
AEMeasurable.sin : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  AEMeasurable f μ → AEMeasurable (fun x => Real.sin (f x)) μ
-- Mathlib.Topology.Order.LowerUpperTopology
/-- The upper closure of a finite set is closed in the lower topology.  -/
Topology.IsLower.isClosed_upperClosure : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsLower α] {s : Set α},
  s.Finite → IsClosed ↑(upperClosure s)
-- Mathlib.Algebra.Order.Ring.Defs
IsStrictOrderedRing.toPosMulStrictMono : ∀ {R : Type u_1} {inst : Semiring R} {inst_1 : PartialOrder R} [self : IsStrictOrderedRing R], PosMulStrictMono R
-- Mathlib.LinearAlgebra.Matrix.Vec
Matrix.vec_single : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : DecidableEq m] [inst_1 : DecidableEq n] [inst_2 : Zero R] (i : m)
  (j : n) (r : R), (Matrix.single i j r).vec = Pi.single (j, i) r
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rcc_eq_toArray_rco : ∀ {m n : ℕ}, (m...=n).toArray = (m...n + 1).toArray
-- Mathlib.Data.Fin.Tuple.Reflection
/-- This can be used to prove
```lean
example [AddCommMonoid α] (a : Fin 3 → α) : ∑ i, a i = a 0 + a 1 + a 2 :=
  (sum_eq _).symm
```  -/
FinVec.sum_eq : ∀ {α : Type u_1} [inst : AddCommMonoid α] {m : ℕ} (a : Fin m → α), FinVec.sum a = ∑ i, a i
-- Mathlib.Data.Finsupp.MonomialOrder.DegLex
/-- The linear order on `Finsupp`s obtained by the homogeneous lexicographic ordering.  -/
Finsupp.DegLex.instLinearOrderDegLexNat : {α : Type u_1} → [LinearOrder α] → LinearOrder (DegLex (α →₀ ℕ))
-- Mathlib.Data.ENNReal.Operations
ENNReal.mul_lt_mul_iff_right : ∀ {a b c : ENNReal}, a ≠ 0 → a ≠ ⊤ → (a * b < a * c ↔ b < c)
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.le_prod_iff : ∀ {N : Type u_2} [inst : MulOneClass N] {M : Type u_5} [inst_1 : MulOneClass M] {s : Submonoid M} {t : Submonoid N}
  {u : Submonoid (M × N)},
  u ≤ s.prod t ↔ Submonoid.map (MonoidHom.fst M N) u ≤ s ∧ Submonoid.map (MonoidHom.snd M N) u ≤ t
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.Hom.ext : ∀ {A : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} A} {B : Type u_2}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} B} {T : Type u_3} {inst_2 : CategoryTheory.Category.{v_3, u_3} T}
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B}
  {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W} {x y : X.Hom Y}, x.left = y.left → x.right = y.right → x = y
-- Mathlib.Tactic.FunProp.Types
Mathlib.Meta.FunProp.Context.mk.inj : ∀ {config : Mathlib.Meta.FunProp.Config} {constToUnfold : Std.TreeSet Lean.Name Lean.Name.quickCmp}
  {disch : Lean.Expr → Lean.MetaM (Option Lean.Expr)} {transitionDepth : ℕ} {config_1 : Mathlib.Meta.FunProp.Config}
  {constToUnfold_1 : Std.TreeSet Lean.Name Lean.Name.quickCmp} {disch_1 : Lean.Expr → Lean.MetaM (Option Lean.Expr)}
  {transitionDepth_1 : ℕ},
  { config := config, constToUnfold := constToUnfold, disch := disch, transitionDepth := transitionDepth } =
      { config := config_1, constToUnfold := constToUnfold_1, disch := disch_1, transitionDepth := transitionDepth_1 } →
    config = config_1 ∧ constToUnfold = constToUnfold_1 ∧ disch = disch_1 ∧ transitionDepth = transitionDepth_1
-- Mathlib.Analysis.Complex.Trigonometric
Complex.sin_ofReal_im : ∀ (x : ℝ), (Complex.sin ↑x).im = 0
-- Lean.Util.ShareCommon
Lean.ShareCommon.PShareCommonM : Type u_1 → Type u_1
-- Init.Data.List.Erase
List.eraseP_eq_self_iff : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, List.eraseP p l = l ↔ ∀ a ∈ l, ¬p a = true
-- Mathlib.CategoryTheory.Limits.Opposites
/-- Turn a limit of `F : Jᵒᵖ ⥤ Cᵒᵖ` into a colimit of `F.unop : J ⥤ C`.  -/
CategoryTheory.Limits.isColimitCoconeUnopOfCone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} J] →
        (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) →
          {c : CategoryTheory.Limits.Cone F} →
            CategoryTheory.Limits.IsLimit c → CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeUnopOfCone c)