mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.ModelTheory.Syntax
_private.Mathlib.ModelTheory.Syntax.0.FirstOrder.Language.Term.varFinsetLeft.match_1.eq_2 : ∀ {L : FirstOrder.Language} {α : Type u_4} {β : Type u_3} (motive : L.Term (α ⊕ β) → Sort u_5) (_i : β)
  (h_1 : (i : α) → motive (FirstOrder.Language.var (Sum.inl i)))
  (h_2 : (_i : β) → motive (FirstOrder.Language.var (Sum.inr _i)))
  (h_3 : (l : ℕ) → (_f : L.Functions l) → (ts : Fin l → L.Term (α ⊕ β)) → motive (FirstOrder.Language.func _f ts)),
  (match FirstOrder.Language.var (Sum.inr _i) with
    | FirstOrder.Language.var (Sum.inl i) => h_1 i
    | FirstOrder.Language.var (Sum.inr _i) => h_2 _i
    | FirstOrder.Language.func _f ts => h_3 l _f ts) =
    h_2 _i
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
Submodule.subtypeₗᵢ_toContinuousLinearMap : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E] {R' : Type u_11} [inst_1 : Ring R'] [inst_2 : Module R' E]
  (p : Submodule R' E), p.subtypeₗᵢ.toContinuousLinearMap = p.subtypeL
-- Mathlib.CategoryTheory.MorphismProperty.Descent
CategoryTheory.MorphismProperty.pullback_snd_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P Q : CategoryTheory.MorphismProperty C} {X Y Z : C}
  {f : X ⟶ Z} {g : Y ⟶ Z} [P.IsStableUnderBaseChange] [P.DescendsAlong Q]
  [inst_3 : CategoryTheory.Limits.HasPullback f g], Q g → (P (CategoryTheory.Limits.pullback.snd f g) ↔ P f)
-- Mathlib.FieldTheory.Differential.Basic
Differential.logDeriv.eq_1 : ∀ {R : Type u_1} [inst : Field R] [inst_1 : Differential R] (a : R), Differential.logDeriv a = a′ / a
-- Init.Data.Array.MapIdx
Array.toList_mapFinIdxM : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {xs : Array α}
  {f : (i : ℕ) → α → i < xs.size → m β}, Array.toList <$> xs.mapFinIdxM f = xs.toList.mapFinIdxM f
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
Polynomial.sylveserMap_comp_adjSylvester : ∀ {m n : ℕ} {R : Type u_1} [inst : CommRing R] (f g : Polynomial R) (hf : f.natDegree ≤ m) (hg : g.natDegree ≤ n),
  f.sylvesterMap g hf hg ∘ₗ f.adjSylvester g = f.resultant g m n • LinearMap.id
-- Mathlib.Analysis.Polynomial.MahlerMeasure
Polynomial.mahlerMeasure_const : ∀ (z : ℂ), (Polynomial.C z).mahlerMeasure = ‖z‖
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  {f : α → β → γ} {k : α}, (Std.TreeMap.map f t).getKey? k = t.getKey? k
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.below.tensorHom_comp_tensorHom : ∀ {C : Type u}
  {motive :
    {X Y : CategoryTheory.FreeMonoidalCategory C} →
      (a a_1 : X.Hom Y) → CategoryTheory.FreeMonoidalCategory.HomEquiv a a_1 → Prop}
  {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : CategoryTheory.FreeMonoidalCategory C} (f₁ : X₁.Hom Y₁) (f₂ : X₂.Hom Y₂) (g₁ : Y₁.Hom Z₁)
  (g₂ : Y₂.Hom Z₂), CategoryTheory.FreeMonoidalCategory.HomEquiv.below ⋯
-- Mathlib.Data.Vector3
_private.Mathlib.Data.Vector3.0.Fin2.insertPerm.match_1.eq_3 : ∀ (motive : (x : ℕ) → Fin2 x → Fin2 x → Sort u_1) (a : ℕ) (a_1 : Fin2 a.succ)
  (h_1 : (n : ℕ) → motive (n + 1) Fin2.fz Fin2.fz) (h_2 : (n : ℕ) → (j : Fin2 n) → motive (n + 1) Fin2.fz j.fs)
  (h_3 : (a : ℕ) → (a_2 : Fin2 a.succ) → motive (a.succ + 1) a_2.fs Fin2.fz)
  (h_4 : (a : ℕ) → (i : Fin2 a.succ) → (j : Fin2 (a + 1)) → motive (a.succ + 1) i.fs j.fs),
  (match a.succ + 1, a_1.fs, Fin2.fz with
    | .(n + 1), Fin2.fz, Fin2.fz => h_1 n
    | .(n + 1), Fin2.fz, j.fs => h_2 n j
    | .(a.succ + 1), a_2.fs, Fin2.fz => h_3 a a_2
    | .(a.succ + 1), i.fs, j.fs => h_4 a i j) =
    h_3 a a_1
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.RingObjCat.Hom.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.CartesianMonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} {R₁ R₂ : CategoryTheory.RingObjCat C} {hom : R₁.X ⟶ R₂.X}
  {isRingHom : CategoryTheory.IsRingHom hom} {hom_1 : R₁.X ⟶ R₂.X} {isRingHom_1 : CategoryTheory.IsRingHom hom_1},
  { hom := hom, isRingHom := isRingHom } = { hom := hom_1, isRingHom := isRingHom_1 } → hom = hom_1
-- Mathlib.Topology.Order.Compact
IsCompact.exists_isGLB : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [ClosedIicTopology α] {s : Set α},
  IsCompact s → s.Nonempty → ∃ x ∈ s, IsGLB s x
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.mk.injEq : ∀ {R : Type u} [inst : NonAssocRing R] (toSubsemiring : Subsemiring R)
  (neg_mem' : ∀ {x : R}, x ∈ toSubsemiring.carrier → -x ∈ toSubsemiring.carrier) (toSubsemiring_1 : Subsemiring R)
  (neg_mem'_1 : ∀ {x : R}, x ∈ toSubsemiring_1.carrier → -x ∈ toSubsemiring_1.carrier),
  ({ toSubsemiring := toSubsemiring, neg_mem' := neg_mem' } =
      { toSubsemiring := toSubsemiring_1, neg_mem' := neg_mem'_1 }) =
    (toSubsemiring = toSubsemiring_1)
-- Lean.Meta.Tactic.AuxLemma
Lean.Meta.AuxLemmas.mk.sizeOf_spec : ∀ (lemmas : Lean.PHashMap Lean.Meta.AuxLemmaKey (Lean.Name × List Lean.Name)),
  sizeOf { lemmas := lemmas } = 1 + sizeOf lemmas
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.delabSort : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- The composition of morphisms of snake inputs.  -/
CategoryTheory.ShortComplex.SnakeInput.Hom.comp : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {S₁ S₂ S₃ : CategoryTheory.ShortComplex.SnakeInput C} → S₁.Hom S₂ → S₂.Hom S₃ → S₁.Hom S₃
-- Mathlib.NumberTheory.FactorisationProperties
Nat.Pseudoperfect.eq_1 : ∀ (n : ℕ), n.Pseudoperfect = (0 < n ∧ ∃ s ⊆ n.properDivisors, ∑ i ∈ s, i = n)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddLocalization.decidableEq.eq_1 : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : IsCancelAdd α] {s : AddSubmonoid α} [inst_2 : DecidableEq α]
  (a b : AddLocalization s),
  a.decidableEq b = a.recOnSubsingleton₂ b fun x x_1 x_2 x_3 => decidable_of_iff' (↑x_3 + x = ↑x_2 + x_1) ⋯
-- Mathlib.Order.Filter.Basic
Filter.eventually_and : ∀ {α : Type u} {p q : α → Prop} {f : Filter α},
  (∀ᶠ (x : α) in f, p x ∧ q x) ↔ (∀ᶠ (x : α) in f, p x) ∧ ∀ᶠ (x : α) in f, q x
-- Mathlib.Data.Set.Image
Set.range_inl : ∀ {α : Type u_1} {β : Type u_2}, Set.range Sum.inl = {x | x.isLeft = true}
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
/-- The preimage of a non-unital subsemiring along a non-unital ring homomorphism is a
non-unital subsemiring.  -/
NonUnitalSubsemiring.comap : {R : Type u} →
  {S : Type v} →
    [inst : NonUnitalNonAssocSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring S] →
        {F : Type u_1} →
          [inst_2 : FunLike F R S] → [NonUnitalRingHomClass F R S] → F → NonUnitalSubsemiring S → NonUnitalSubsemiring R
-- Mathlib.Data.FunLike.IsApply
/-- **Alias** of `IsSMulApply.smul_apply`. -/
smul_apply : ∀ {M : Type u_1} {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} {inst : FunLike F α β}
  {inst_1 : SMul M β} {inst_2 : SMul M F} [self : IsSMulApply M F α β] (f : F) (r : M) (x : α), (r • f) x = r • f x
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.casesOn_mk' : ∀ {F : PFunctor.{uA, uB}} {r : F.M → Sort u_2} {a : F.A} (x : F.B a → F.M)
  (f : (a : F.A) → (f : F.B a → F.M) → r (PFunctor.M.mk ⟨a, f⟩)), (PFunctor.M.mk ⟨a, x⟩).casesOn' f = f a x
-- Mathlib.Algebra.BigOperators.GroupWithZero.Action
Finset.smul_sum : ∀ {M : Type u_1} {N : Type u_2} {γ : Type u_3} [inst : AddCommMonoid N] [inst_1 : DistribSMul M N] {r : M} {f : γ → N}
  {s : Finset γ}, r • ∑ x ∈ s, f x = ∑ x ∈ s, r • f x
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidIso.val_inv_unitsWithZero_symm_apply : ∀ {α : Type u_6} [inst : Group α] [inst_1 : Preorder α] (a : α), ↑(OrderMonoidIso.unitsWithZero.symm a)⁻¹ = (↑a)⁻¹
-- Mathlib.Geometry.Manifold.VectorBundle.Hom
/-- Consider `C^n` maps `v : M → E₁` and `w : M → E₂` to vector bundles, over a base map
`b : M → B`, and bilinear maps `ψ m : E₁ (b m) → E₂ (b m) → E₃ (b m)` depending smoothly on `m`.
One can apply `ψ  m` to `v m` and `w m`, and the resulting map is `C^n`.

We give here a version of this statement on a set.  -/
ContMDiffOn.clm_bundle_apply₂ : ∀ {𝕜 : Type u_1} {B : Type u_2} {F₁ : Type u_3} {F₂ : Type u_4} {F₃ : Type u_5} {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)] {E₃ : B → Type u_9} [inst_13 : (x : B) → AddCommGroup (E₃ x)]
  [inst_14 : (x : B) → Module 𝕜 (E₃ x)] [inst_15 : NormedAddCommGroup F₃] [inst_16 : NormedSpace 𝕜 F₃]
  [inst_17 : TopologicalSpace (Bundle.TotalSpace F₃ E₃)] [inst_18 : (x : B) → TopologicalSpace (E₃ x)] {EB : Type u_10}
  [inst_19 : NormedAddCommGroup EB] [inst_20 : NormedSpace 𝕜 EB] {HB : Type u_11} [inst_21 : TopologicalSpace HB]
  {IB : ModelWithCorners 𝕜 EB HB} [inst_22 : TopologicalSpace B] [inst_23 : ChartedSpace HB B] {EM : Type u_12}
  [inst_24 : NormedAddCommGroup EM] [inst_25 : NormedSpace 𝕜 EM] {HM : Type u_13} [inst_26 : TopologicalSpace HM]
  {IM : ModelWithCorners 𝕜 EM HM} [inst_27 : TopologicalSpace M] [inst_28 : ChartedSpace HM M]
  [inst_29 : FiberBundle F₁ E₁] [inst_30 : VectorBundle 𝕜 F₁ E₁] [inst_31 : FiberBundle F₂ E₂]
  [inst_32 : VectorBundle 𝕜 F₂ E₂] [inst_33 : FiberBundle F₃ E₃] [inst_34 : ⋯], ⋯
-- Mathlib.Analysis.Calculus.ContDiff.Comp
ContDiffAt.smulRight : ∀ {𝕜 : 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] {x : E} {n : WithTop ℕ∞} {f : E → StrongDual 𝕜 F}
  {g : E → G},
  ContDiffAt 𝕜 n f x → ContDiffAt 𝕜 n g x → ContDiffAt 𝕜 n (fun x => ContinuousLinearMap.smulRight (f x) (g x)) x
-- Mathlib.Logic.Equiv.Basic
Equiv.image_swap_of_mem_of_notMem : ∀ {α : Type u_9} [inst : DecidableEq α] {s : Set α} {i j : α}, i ∈ s → j ∉ s → ⇑(Equiv.swap i j) '' s = insert j s \ {i}
-- Mathlib.LinearAlgebra.Finsupp.Span
Finsupp.lsingle_range_le_ker_lapply : ∀ {α : Type u_1} {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (s t : Set α), Disjoint s t → ⨆ a ∈ s, (Finsupp.lsingle a).range ≤ ⨅ a ∈ t, (Finsupp.lapply a).ker
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.homMk_τ₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (τ₁ : S₁.X₁ ⟶ S₂.X₁) (τ₂ : S₁.X₂ ⟶ S₂.X₂) (τ₃ : S₁.X₃ ⟶ S₂.X₃)
  (comm₁₂ : CategoryTheory.CategoryStruct.comp τ₁ S₂.f = CategoryTheory.CategoryStruct.comp S₁.f τ₂)
  (comm₂₃ : CategoryTheory.CategoryStruct.comp τ₂ S₂.g = CategoryTheory.CategoryStruct.comp S₁.g τ₃),
  (CategoryTheory.ShortComplex.homMk τ₁ τ₂ τ₃ comm₁₂ comm₂₃).τ₁ = τ₁
-- Mathlib.Combinatorics.Matroid.Circuit
/-- For `I` independent, `M.fundCircuit e I` is the only circuit contained in `insert e I`.  -/
Matroid.IsCircuit.eq_fundCircuit_of_subset : ∀ {α : Type u_1} {M : Matroid α} {C I : Set α} {e : α},
  M.IsCircuit C → M.Indep I → C ⊆ insert e I → C = M.fundCircuit e I
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.exp_map_apply : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieAlgebra ℚ L] (D : LieDerivation R L L) (h : IsNilpotent ↑D) (l : L), (D.exp h) l = (IsNilpotent.exp ↑D) l
-- Mathlib.Data.Finset.Image
Finset.image_comp_eq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : DecidableEq β] {f : α → β} [inst_1 : DecidableEq γ] {g : β → γ},
  Finset.image (g ∘ f) = Finset.image g ∘ Finset.image f
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.checkColGt.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.toLp_fst : ∀ {p : ENNReal} {α : Type u_2} {β : Type u_3} (x : α × β), (WithLp.toLp p x).fst = x.1
-- Mathlib.Data.Fintype.BigOperators
Fintype.prod_eq_mul : ∀ {α : Type u_1} {M : Type u_4} [inst : Fintype α] [inst_1 : CommMonoid M] {f : α → M} (a b : α),
  a ≠ b → (∀ (x : α), x ≠ a ∧ x ≠ b → f x = 1) → ∏ x, f x = f a * f b
-- Std.Data.Iterators.Lemmas.Equivalence.Basic
Std.IterM.Equiv.of_morphism : ∀ {α₁ α₂ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : LawfulMonad m] {β : Type w}
  [inst_2 : Std.Iterator α₁ m β] [inst_3 : Std.Iterator α₂ m β] (ita : Std.IterM m β)
  (f : Std.IterM m β → Std.IterM m β),
  (∀ (it : Std.IterM m β), (f it).stepAsHetT = Std.IterStep.mapIterator f <$> it.stepAsHetT) → ita.Equiv (f ita)
-- Lean.Meta.MethodSpecs
_private.Lean.Meta.MethodSpecs.0.Lean.rewriteThm : Lean.Meta.Simp.Context → Lean.Meta.Simprocs → Lean.Name → Lean.Name → Lean.MetaM Unit
-- Mathlib.Algebra.Ring.GeomSum
geom_sum_Ico_mul_neg : ∀ {R : Type u_1} [inst : Ring R] (x : R) {m n : ℕ}, m ≤ n → (∑ i ∈ Finset.Ico m n, x ^ i) * (1 - x) = x ^ m - x ^ n
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
Nat.reducePow : Lean.Meta.Simp.DSimproc
-- Mathlib.FieldTheory.RatFunc.Luroth
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.Φ_coeff_generatorIndex_ne_zero : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)} (h : E ≠ ⊥),
  (RatFunc.Luroth.Φ✝ E).coeff (RatFunc.Luroth.generatorIndex✝ h) ≠ 0
-- Init.Prelude
/-- Retrieves the local value.  -/
MonadReaderOf.read : {ρ : semiOutParam (Type u)} → {m : Type u → Type v} → [self : MonadReaderOf ρ m] → m ρ
-- Mathlib.RingTheory.Ideal.Pure
Ideal.Pure.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R), I.Pure = Module.Flat R (R ⧸ I)
-- Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltered_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  {N : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} N] (p : CategoryTheory.Functor N C)
  [inst_3 : CategoryTheory.InitiallySmall N] {J : CategoryTheory.GrothendieckTopology C}
  [inst_4 : CategoryTheory.IsCofiltered N]
  (hp :
    ∀ ⦃X : C⦄,
      ∀ R ∈ J X,
        ∀ ⦃U : N⦄ (f : p.obj U ⟶ X),
          ∃ Y g,
            ∃ (_ : R.arrows g),
              ∃ V q a, CategoryTheory.CategoryStruct.comp a g = CategoryTheory.CategoryStruct.comp (p.map q) f)
  {A : Type u''} [inst_5 : CategoryTheory.Category.{v'', u''} A]
  [inst_6 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] {P Q : CategoryTheory.Functor Cᵒᵖ A} (g : P ⟶ Q)
  (U : N) {Z : A} (h : (CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered p hp).presheafFiber.obj Q ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltered p hp U P)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered p hp).presheafFiber.map g) h) =
    CategoryTheory.CategoryStruct.comp (g.app (Opposite.op (p.obj U)))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltered p hp U Q) h)
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.transIsEquivalentIsLittleO : {α : Type u_1} →
  {β : Type u_2} →
    {β₂ : Type u_3} →
      [inst : NormedAddCommGroup β] →
        [inst_1 : Norm β₂] →
          {l : Filter α} → Trans (Asymptotics.IsEquivalent l) (Asymptotics.IsLittleO l) (Asymptotics.IsLittleO l)
-- Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
CategoryTheory.PreOneHypercover.cylinder_X : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} [inst_1 : CategoryTheory.Limits.HasPullbacks C] (f g : E.Hom F)
  (p : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)),
  (CategoryTheory.PreOneHypercover.cylinder f g).X p = CategoryTheory.PreOneHypercover.cylinderX f g p.snd
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
CategoryTheory.CostructuredArrow.ιCompGrothendieckPrecompFunctorToCommaCompFst_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D)
  (R : CategoryTheory.Functor E D) (X : E) (X_1 : ↑((R.comp (CategoryTheory.CostructuredArrow.functor L)).obj X)),
  (CategoryTheory.CostructuredArrow.ιCompGrothendieckPrecompFunctorToCommaCompFst L R X).hom.app X_1 =
    CategoryTheory.CategoryStruct.id (CategoryTheory.CostructuredArrow.left X_1)
-- Mathlib.Data.Multiset.Filter
Multiset.mem_filterMap : ∀ {α : Type u_1} {β : Type v} (f : α → Option β) (s : Multiset α) {b : β},
  b ∈ Multiset.filterMap f s ↔ ∃ a ∈ s, f a = some b
-- Lean.Data.Lsp.Window
Lean.Lsp.instToJsonMessageType : Lean.ToJson Lean.Lsp.MessageType
-- Std.Async.IO
Std.Async.IO.AsyncWrite.write : {α β : Type} → [self : Std.Async.IO.AsyncWrite α β] → α → β → Std.Async.Async Unit
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.coeff_ofFinsupp : ∀ {R : Type u} [inst : Semiring R] (p : AddMonoidAlgebra R ℕ), { toFinsupp := p }.coeff = ⇑p.coeff
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.ext : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {h h' : X ≃ₜ Y},
  (∀ (x : X), h x = h' x) → h = h'
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKeyD_filter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : α → β → Bool} {k fallback : α} (h : (↑m).WF),
  (Std.DHashMap.Internal.Raw₀.filter f m).getKeyD k fallback =
    ((m.getKey? k).pfilter fun x h' => f x (Std.DHashMap.Internal.Raw₀.Const.get m x ⋯)).getD fallback
-- Mathlib.Algebra.Module.Lattice
/-- The action of `Aˣ` on `R`-submodules of `V` preserves `IsLattice`.  -/
Submodule.IsLattice.smul : ∀ {R : Type u_1} [inst : CommRing R] (A : Type u_2) [inst_1 : CommRing A] [inst_2 : Algebra R A] {V : Type u_3}
  [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : Module A V] [inst_6 : IsScalarTower R A V]
  (M : Submodule R V) [Submodule.IsLattice A M] (a : Aˣ), Submodule.IsLattice A (a • M)
-- Mathlib.RingTheory.Localization.AsSubring
Localization.subalgebra.isFractionRing : ∀ {A : Type u_1} (K : Type u_2) [inst : CommRing A] (S : Submonoid A) (hS : S ≤ nonZeroDivisors A) [inst_1 : CommRing K]
  [inst_2 : Algebra A K] [inst_3 : IsFractionRing A K], IsFractionRing (↥(Localization.subalgebra K S hS)) K
-- Mathlib.LinearAlgebra.TensorProduct.Basic
/-- If M and N are both R- and A-modules and their actions on them commute,
and if the A-action on `M ⊗[R] N` can switch between the two factors, then there is a
canonical S-linear map from `M ⊗[A] N` to `M ⊗[R] N`,
where `S` is any other ring acting on `M` and whose action commutes with the `A` and `R`-actions.  -/
TensorProduct.mapOfCompatibleSMul : (R : Type u_1) →
  [inst : CommSemiring R] →
    (A : Type u_22) →
      (S : Type u_23) →
        (M : Type u_24) →
          (N : Type u_25) →
            [inst_1 : AddCommMonoid M] →
              [inst_2 : AddCommMonoid N] →
                [inst_3 : Module R M] →
                  [inst_4 : Module R N] →
                    [inst_5 : CommSemiring A] →
                      [inst_6 : Module A M] →
                        [inst_7 : Module A N] →
                          [SMulCommClass R A M] →
                            [inst_9 : CommSemiring S] →
                              [inst_10 : Module S M] →
                                [inst_11 : SMulCommClass R S M] →
                                  [inst_12 : SMulCommClass A S M] →
                                    [TensorProduct.CompatibleSMul R A M N] →
                                      TensorProduct A M N →ₗ[S] TensorProduct R M N
-- Lean.Linter.Init
Lean.Linter.LinterSetsState.mk.inj : ∀ {merged : Lean.Linter.LinterSets} {localEntries : Array (Lean.Name × Lean.NameSet)}
  {merged_1 : Lean.Linter.LinterSets} {localEntries_1 : Array (Lean.Name × Lean.NameSet)},
  { merged := merged, localEntries := localEntries } = { merged := merged_1, localEntries := localEntries_1 } →
    merged = merged_1 ∧ localEntries = localEntries_1
-- Mathlib.RingTheory.Invariant.Profinite
/-- (Implementation)
The functor taking an open normal subgroup `N ≤ G` to the set of lifts of `σ` in `G ⧸ N`.
We will show that its inverse limit is nonempty to conclude that there exists a lift in `G`.  -/
Ideal.Quotient.stabilizerHomSurjectiveAuxFunctor : {A : Type u_1} →
  {B : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : CommRing B] →
        [inst_2 : Algebra A B] →
          {G : Type u} →
            [inst_3 : Group G] →
              [inst_4 : MulSemiringAction G B] →
                [SMulCommClass G A B] →
                  [inst_6 : TopologicalSpace G] →
                    (P : Ideal A) →
                      (Q : Ideal B) →
                        [inst_7 : Q.LiesOver P] →
                          ((B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q) → CategoryTheory.Functor (OpenNormalSubgroup G) (Type u)
-- Mathlib.Algebra.DirectSum.Internal
SetLike.Homogeneous.smul : ∀ {ι : Type u_1} {S : Type u_3} {R : Type u_4} [inst : CommSemiring S] [inst_1 : Semiring R] [inst_2 : Algebra S R]
  {A : ι → Submodule S R} {s : S} {r : R}, SetLike.IsHomogeneousElem A r → SetLike.IsHomogeneousElem A (s • r)
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
/-- Summand in the series for the `z`-derivative of the Jacobi theta function.  -/
jacobiTheta₂'_term : ℤ → ℂ → ℂ → ℂ
-- Mathlib.Tactic.ClickSuggestions.TryPremises
_private.Mathlib.Tactic.ClickSuggestions.TryPremises.0.Mathlib.Tactic.ClickSuggestions.Candidates.appAt.sizeOf_spec : ∀ (arr : Array Mathlib.Tactic.ClickSuggestions.ApplyAtLemma),
  sizeOf (Mathlib.Tactic.ClickSuggestions.Candidates.appAt✝ arr) = 1 + sizeOf arr
-- Init.Data.BitVec.Lemmas
/-- `x.shiftConcat b` does not overflow if `x < 2^k` for `k < w`, and so
`x.shiftConcat b |>.toNat = x.toNat * 2 + b.toNat`.  -/
BitVec.toNat_shiftConcat_eq_of_lt : ∀ {w : ℕ} {x : BitVec w} {b : Bool} {k : ℕ}, k < w → x.toNat < 2 ^ k → (x.shiftConcat b).toNat = x.toNat * 2 + b.toNat
-- Mathlib.Algebra.Homology.HomotopyCofiber
/-- Auxiliary definition for `mapHomologicalComplexObjIso`.  -/
HomologicalComplex.homotopyCofiber.mapHomologicalComplexObjXIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          {F G : HomologicalComplex C c} →
            (φ : F ⟶ G) →
              [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] →
                [inst_3 : DecidableRel c.Rel] →
                  {D : Type u_3} →
                    [inst_4 : CategoryTheory.Category.{v_2, u_3} D] →
                      [inst_5 : CategoryTheory.Preadditive D] →
                        (H : CategoryTheory.Functor C D) →
                          [inst_6 : H.Additive] →
                            [inst_7 : HomologicalComplex.HasHomotopyCofiber ((H.mapHomologicalComplex c).map φ)] →
                              (i : ι) →
                                H.obj ((HomologicalComplex.homotopyCofiber φ).X i) ≅
                                  (HomologicalComplex.homotopyCofiber ((H.mapHomologicalComplex c).map φ)).X i
-- Mathlib.Topology.VectorBundle.Basic
VectorBundleCore.trivializationAt_coordChange_eq : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField R] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace R F] [inst_3 : TopologicalSpace B] {ι : Type u_5} (Z : VectorBundleCore R B F ι) {b₀ b₁ b : B},
  b ∈ (trivializationAt F Z.Fiber b₀).baseSet ∩ (trivializationAt F Z.Fiber b₁).baseSet →
    ∀ (v : F),
      (Bundle.Trivialization.coordChangeL R (trivializationAt F Z.Fiber b₀) (trivializationAt F Z.Fiber b₁) b) v =
        (Z.coordChange (Z.indexAt b₀) (Z.indexAt b₁) b) v