mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Data.List.Lemmas
List.idxOfNth_lt_idxOfNth_iff_of_lt_count : ∀ {α : Type u_1} {n : ℕ} {x : α} {m : ℕ} [inst : BEq α] {xs : List α},
  n < List.count x xs → (List.idxOfNth x xs n < List.idxOfNth x xs m ↔ n < m)
-- Init.Data.Range.Polymorphic.Internal.SignedBitVec
_private.Init.Data.Range.Polymorphic.Internal.SignedBitVec.0.BitVec.Signed.rotate_intMinSealed : ∀ {n : ℕ}, BitVec.Signed.rotate✝ (BitVec.Signed.intMinSealed✝ n) = ↑0
-- Init.Data.List.Basic
/-- A nonempty list is pairwise related with `R` if the head is related to every element of the tail
and the tail is itself pairwise related.

That is, `a :: l` is `Pairwise R` if:
 * `R` relates `a` to every element of `l`
 * `l` is `Pairwise R`.
 -/
List.Pairwise.cons : ∀ {α : Type u} {R : α → α → Prop} {a : α} {l : List α},
  (∀ a' ∈ l, R a a') → List.Pairwise R l → List.Pairwise R (a :: l)
-- Mathlib.Topology.Instances.Matrix
/-- **Alias** of `isClosed_setOfPred_blockTriangular`. -/
isClosed_setOf_blockTriangular : ∀ {m : Type u_4} {R : Type u_8} [inst : TopologicalSpace R] {α : Type u_11} {b : m → α} [inst_1 : LinearOrder α]
  [inst_2 : Zero R] [T2Space R], IsClosed {M | M.BlockTriangular b}
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.eventually_exp_le : ∀ {u : ℕ → ENNReal} {a : EReal}, a < ExpGrowth.expGrowthInf u → ∀ᶠ (n : ℕ) in Filter.atTop, (a * ↑n).exp ≤ u n
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
Submodule.orthogonal_closure' : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) (x : E), (∀ y ∈ K, inner 𝕜 y x = 0) ↔ ∀ y ∈ K.topologicalClosure, inner 𝕜 y x = 0
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
MeasureTheory.charFun_zero : ∀ {E : Type u_2} {mE : MeasurableSpace E} [inst : SeminormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E]
  (μ : MeasureTheory.Measure E), MeasureTheory.charFun μ 0 = ↑(μ.real Set.univ)
-- Mathlib.Logic.Equiv.Option
/-- The set of `x : Option α` such that `isSome x` is equivalent to `α`.  -/
Equiv.optionIsSomeEquiv : (α : Type u_4) → { x // x.isSome = true } ≃ α
-- Mathlib.Order.LiminfLimsup
Filter.limsup_sdiff : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteBooleanAlgebra α] (f : Filter β) (u : β → α) (a : α),
  Filter.limsup u f \ a = Filter.limsup (fun b => u b \ a) f
-- Lean.Elab.PreDefinition.Structural.IndGroupInfo
Lean.Elab.Structural.IndGroupInfo.ofInductiveVal : Lean.InductiveVal → Lean.Elab.Structural.IndGroupInfo
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.foldlM_eq_foldlM_toArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {δ : Type w}
  {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] {f : δ → (a : α) → β a → m δ} {init : δ},
  Std.DTreeMap.Raw.foldlM f init t = Array.foldlM (fun a b => f a b.fst b.snd) init t.toArray
-- Mathlib.Order.Category.NonemptyFinLinOrd
NonemptyFinLinOrd.epi_iff_surjective : ∀ {A B : NonemptyFinLinOrd} (f : A ⟶ B),
  CategoryTheory.Epi f ↔ Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
/-- In a fiber bundle, the preimage under the projection of a set with unique differentials
in the base has unique differentials in the bundle.  -/
UniqueMDiffWithinAt.bundle_preimage : ∀ {𝕜 : 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] {s : Set M} {F : Type u_9} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {Z : M → Type u_10} [inst_8 : TopologicalSpace (Bundle.TotalSpace F Z)]
  [inst_9 : (b : M) → TopologicalSpace (Z b)] [inst_10 : FiberBundle F Z] {p : Bundle.TotalSpace F Z},
  UniqueMDiffAt[s] p.proj → UniqueMDiffAt[Bundle.TotalSpace.proj ⁻¹' s] p
-- Mathlib.CategoryTheory.Yoneda
/-- `FullyFaithful.homEquiv` as a natural isomorphism, using coyoneda.  -/
CategoryTheory.Functor.FullyFaithful.compUliftCoyonedaCompWhiskeringLeft : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          F.FullyFaithful →
            (F.op.comp
                (CategoryTheory.uliftCoyoneda.{v₁, v₂, u₂}.comp
                  ((CategoryTheory.Functor.whiskeringLeft C D (Type (max v₁ v₂))).obj F)) ≅
              CategoryTheory.uliftCoyoneda.{v₂, v₁, u₁})
-- Mathlib.Dynamics.PeriodicPts.Defs
MulAction.zpow_add_period_smul : ∀ {α : Type v} {G : Type u} [inst : Group G] [inst_1 : MulAction G α] (i : ℤ) (g : G) (a : α),
  g ^ (i + ↑(MulAction.period g a)) • a = g ^ i • a
-- Mathlib.CategoryTheory.Localization.Construction
/-- The function `(W.FunctorsInverting D) ⥤ (W.Localization ⥤ D)` induced by
`Construction.lift`.  -/
CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    (W : CategoryTheory.MorphismProperty C) →
      (D : Type uD) →
        [inst_1 : CategoryTheory.Category.{uD', uD} D] →
          CategoryTheory.Functor (W.FunctorsInverting D) (CategoryTheory.Functor W.Localization D)
-- Init.Grind.Order
Lean.Grind.Order.le_eq_true_of_le_k : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [inst_3 : Std.IsPreorder α]
  [inst_4 : Lean.Grind.Ring α] [Lean.Grind.OrderedRing α] {a b : α} {k₁ k₂ : ℤ},
  k₁.ble' k₂ = true → a ≤ b + ↑k₁ → (a ≤ b + ↑k₂) = True
-- Aesop.Tree.RunMetaM
Aesop.Goal.runMetaMInPostNormState' : {m : Type → Type} →
  [Monad m] →
    [MonadLiftT Lean.MetaM m] →
      [MonadFinally m] → {α : Type} → [Lean.MonadError m] → (Lean.MVarId → m α) → Aesop.Goal → m α
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.currying_counitIso_hom_app_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] (X : CategoryTheory.Functor (C × D) E) (X_1 : C × D),
  (CategoryTheory.Functor.currying.counitIso.hom.app X).app X_1 =
    CategoryTheory.CategoryStruct.id (X.obj (X_1.1, X_1.2))
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Finset.compl_truncatedInf : ∀ {α : Type u_1} [inst : BooleanAlgebra α] [inst_1 : DecidableLE α] (s : Finset α) (a : α),
  (s.truncatedInf a)ᶜ = s.compls.truncatedSup aᶜ
-- Mathlib.Order.SuccPred.Tree
/-- The type of rooted trees.
 -/
RootedTree : Type (u_2 + 1)
-- Mathlib.Data.Multiset.ZeroCons
Multiset.Rel.below : {α : Type u_1} →
  {β : Type v} →
    {r : α → β → Prop} →
      {motive : (a : Multiset α) → (a_1 : Multiset β) → Multiset.Rel r a a_1 → Prop} →
        {a : Multiset α} → {a_1 : Multiset β} → Multiset.Rel r a a_1 → Prop
-- Batteries.Data.UnionFind.Basic
/-- Root of a union-find node. Panics if index is out of bounds.  -/
Batteries.UnionFind.root! : Batteries.UnionFind → ℕ → ℕ
-- Mathlib.CategoryTheory.Localization.Bousfield
CategoryTheory.ObjectProperty.isoClosure_isColocal : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C),
  P.isoClosure.isColocal = P.isColocal
-- Mathlib.Data.Seq.Computation
_private.Mathlib.Data.Seq.Computation.0.Computation.BisimO.match_1.splitter : {α : Type u_1} →
  (motive : α ⊕ Computation α → α ⊕ Computation α → Sort u_2) →
    (x x_1 : α ⊕ Computation α) →
      ((a a' : α) → motive (Sum.inl a) (Sum.inl a')) →
        ((s s' : Computation α) → motive (Sum.inr s) (Sum.inr s')) →
          ((x x_2 : α ⊕ Computation α) →
              (∀ (a a' : α), x = Sum.inl a → x_2 = Sum.inl a' → False) →
                (∀ (s s' : Computation α), x = Sum.inr s → x_2 = Sum.inr s' → False) → motive x x_2) →
            motive x x_1
-- Mathlib.GroupTheory.Index
Subgroup.finiteIndex_of_finite_quotient : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} [Finite (G ⧸ H)], H.FiniteIndex
-- Mathlib.Order.Filter.Bases.Basic
Filter.hasBasis_iSup : ∀ {α : Type u_1} {ι : Sort u_6} {ι' : ι → Type u_7} {l : ι → Filter α} {p : (i : ι) → ι' i → Prop}
  {s : (i : ι) → ι' i → Set α},
  (∀ (i : ι), (l i).HasBasis (p i) (s i)) → (⨆ i, l i).HasBasis (fun f => ∀ (i : ι), p i (f i)) fun f => ⋃ i, s i (f i)
-- Mathlib.Order.BoundedOrder.Lattice
bot_inf_eq : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] (a : α), ⊥ ⊓ a = ⊥
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.instNormedRing : {α : Type u_1} →
  [inst : TopologicalSpace α] → [CompactSpace α] → {R : Type u_4} → [inst_2 : NormedRing R] → NormedRing C(α, R)
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
linearIndependent_finSnoc : ∀ {K : Type u_3} {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {x : V} {n : ℕ}
  {v : Fin n → V}, LinearIndependent K (Fin.snoc v x) ↔ LinearIndependent K v ∧ x ∉ Submodule.span K (Set.range v)
-- Qq.MatchImpl
Qq.Impl.mkIsDefEqType : List Qq.Impl.PatVarDecl → Q(Type)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.isNone_getElem?_toArray_roc_eq : ∀ {m n : ℤ} {i : ℕ}, ((m<...=n).toArray[i]?.isNone = true) = ((n - m).toNat ≤ i)
-- Mathlib.Analysis.InnerProductSpace.Subspace
Orthonormal.orthogonalFamily : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {v : ι → E} (hv : Orthonormal 𝕜 v),
  OrthogonalFamily 𝕜 (fun _i => 𝕜) fun i => LinearIsometry.toSpanSingleton 𝕜 E ⋯
-- Mathlib.GroupTheory.Congruence.Defs
/-- Multiplicative congruence relations preserve division.  -/
Con.div : ∀ {M : Type u_1} [inst : Group M] (c : Con M) {w x y z : M}, c w x → c y z → c (w / y) (x / z)
-- Init.PropLemmas
and_and_left : ∀ {a b c : Prop}, a ∧ b ∧ c ↔ (a ∧ b) ∧ a ∧ c
-- Mathlib.Algebra.GroupWithZero.Subgroup
AddSubgroup.pointwise_smul_def : ∀ {M : Type u_3} {A : Type u_4} [inst : Monoid M] [inst_1 : AddGroup A] [inst_2 : DistribMulAction M A] {a : M}
  (S : AddSubgroup A), a • S = AddSubgroup.map ((DistribMulAction.toAddMonoidEnd M A) a) S
-- Mathlib.Tactic.Widget.StringDiagram
/-- The domain of the 2-morphism associated with a node as a list
(the first component is the node itself).  -/
Mathlib.Tactic.Widget.StringDiagram.Node.srcList : Mathlib.Tactic.Widget.StringDiagram.Node →
  List (Mathlib.Tactic.Widget.StringDiagram.Node × Mathlib.Tactic.BicategoryLike.Atom₁)
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.Completion.isometry_toCompletion : ∀ {K : Type u_1} [inst : Field K] (v : NumberField.InfinitePlace K),
  Isometry NumberField.InfinitePlace.Completion.toCompletion
-- Mathlib.GroupTheory.OrderOfElement
AddSemiconjBy.addOrderOf_eq : ∀ {G : Type u_1} [inst : AddGroup G] (a : G) {x y : G}, AddSemiconjBy a x y → addOrderOf x = addOrderOf y
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.coe_mk : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : Bot α] [inst_2 : Max β] [inst_3 : Bot β] (f : SupHom α β)
  (hf : f.toFun ⊥ = ⊥), ⇑{ toSupHom := f, map_bot' := hf } = ⇑f
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
IntermediateField.algebraAdjoinAdjoin.coe_algebraMap : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (S : Set E)
  (x : ↥(Algebra.adjoin F S)), ↑((algebraMap ↥(Algebra.adjoin F S) ↥(IntermediateField.adjoin F S)) x) = ↑x
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Sphere.ext : ∀ {P : Type u_2} {inst : MetricSpace P} {x y : EuclideanGeometry.Sphere P},
  x.center = y.center → x.radius = y.radius → x = y
-- Init.Data.Vector.Lemmas
Vector.getElem_replace_of_ne : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {n : ℕ} {a b : α} {xs : Vector α n} {i : ℕ} {h : i < n},
  xs[i] ≠ a → (xs.replace a b)[i] = xs[i]
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
SimpleGraph.TripartiteFromTriangles.Graph.in₁₀_iff' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {a : α} {b : β},
  (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₁ b) (Sum3.in₀ a) ↔ ∃ x ∈ t, x.2.1 = b ∧ x.1 = a
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Path.map_injective : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} (hinj : Function.Injective ⇑f)
  (u v : V), Function.Injective (SimpleGraph.Path.map f hinj)
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.congrLeftRingEquiv_symm_apply_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {Z : Type u_6}
  [inst_2 : Semiring Z] (e : X ≃ₜ Y) (g : LocallyConstant Y Z) (a : X),
  ((LocallyConstant.congrLeftRingEquiv e).symm g) a = g (e a)
-- Init.Grind.Ring.CommSemiringAdapter
_private.Init.Grind.Ring.CommSemiringAdapter.0.Lean.Grind.CommRing.Expr.denoteS.match_1.eq_9 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (k : ℤ) (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k))
  (h_2 : (k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k))
  (h_3 : (v : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var v))
  (h_4 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_5 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b))
  (h_6 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k))
  (h_7 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b)) (h_8 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_9 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k)),
  (match Lean.Grind.CommRing.Expr.intCast k with
    | Lean.Grind.CommRing.Expr.num k => h_1 k
    | Lean.Grind.CommRing.Expr.natCast k => h_2 k
    | Lean.Grind.CommRing.Expr.var v => h_3 v
    | a.add b => h_4 a b
    | a.mul b => h_5 a b
    | a.pow k => h_6 a k
    | a.sub b => h_7 a b
    | a.neg => h_8 a
    | Lean.Grind.CommRing.Expr.intCast k => h_9 k) =
    h_9 k
-- Mathlib.Order.Circular
OrderDual.circularPreorder : (α : Type u_1) → [CircularPreorder α] → CircularPreorder αᵒᵈ
-- Mathlib.Algebra.Module.SpanRank
/-- Constructs a generating set with cardinality equal to the `spanRank` of the submodule  -/
Submodule.exists_span_set_card_eq_spanRank : ∀ {R : Type u_1} {M : Type u} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (p : Submodule R M),
  ∃ s, Cardinal.mk ↑s = p.spanRank ∧ Submodule.span R s = p
-- Mathlib.NumberTheory.ModularForms.QExpansion
/-- **Alias** of `ModularForm.qExpansion_sub`. -/
ModularFormClass.qExpansion_sub : ∀ {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} {G : Type u_2}
  [inst_1 : FunLike G UpperHalfPlane ℂ],
  0 < h →
    h ∈ Γ.strictPeriods →
      ∀ {a b : ℤ} (f : F) [ModularFormClass F Γ a] (g : G) [ModularFormClass G Γ b],
        UpperHalfPlane.qExpansion h (⇑f - ⇑g) = UpperHalfPlane.qExpansion h ⇑f - UpperHalfPlane.qExpansion h ⇑g
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.subsemigroup_strictAnti : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M],
  StrictAnti ArchimedeanClass.subsemigroup
-- Mathlib.Data.Num.Lemmas
PosNum.to_nat_pos : ∀ (n : PosNum), 0 < ↑n
-- Init.Data.Iterators.Consumers.Monadic.Partial
Std.IterM.Partial.mk.sizeOf_spec : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : SizeOf α] [inst_1 : (a : Type w) → SizeOf (m a)]
  [inst_2 : SizeOf β] (it : Std.IterM m β), sizeOf { it := it } = 1 + sizeOf it
-- Init.Data.List.Basic
List.instEmptyCollection : {α : Type u} → EmptyCollection (List α)
-- Std.Do.Internal.Ensures.Lemmas
Std.Do.Internal.MayReturn.canReturn_eq : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] [LawfulMonad m] [inst_2 : MonadAttach m]
  [LawfulMonadAttach m] (x : m α), MonadAttach.CanReturn x = Std.Do.Internal.MayReturn x
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.Hom.partialIso_target : ∀ {X U : AlgebraicGeometry.Scheme} (f : U ⟶ X) [inst : AlgebraicGeometry.IsOpenImmersion f]
  [inst_1 : AlgebraicGeometry.IsDominant f],
  (AlgebraicGeometry.Scheme.Hom.partialIso f).target =
    ((AlgebraicGeometry.Scheme.Hom.opensRange f).partialIsoOfDense ⋯).target
-- Mathlib.RingTheory.Idempotents
CompleteOrthogonalIdempotents.map : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) {I : Type u_3} {e : I → R}
  [inst_2 : Fintype I], CompleteOrthogonalIdempotents e → CompleteOrthogonalIdempotents (⇑f ∘ e)
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.subLeft_apply : ∀ {G : Type w} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G] (x b : G),
  (Homeomorph.subLeft x) b = x - b
-- Mathlib.Analysis.InnerProductSpace.Defs
/-- Seminormed space core structure constructed from a `PreInnerProductSpace.Core` structure  -/
InnerProductSpace.Core.toSeminormedSpaceCore : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  (c : PreInnerProductSpace.Core 𝕜 F), SeminormedSpace.Core 𝕜 F
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
/-- The natural equivariant map from `n ↪ α` to `m ↪ α` given by an embedding
`e : m ↪ n`.  -/
MulActionHom.embMap : (G : Type u_1) →
  (α : Type u_2) →
    [inst : Group G] → [inst_1 : MulAction G α] → {m : Type u_5} → {n : Type u_6} → (m ↪ n) → (n ↪ α) →ₑ[id] m ↪ α
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Eta-expanded form of `DifferentiableWithinAt.sub` -/
DifferentiableWithinAt.fun_sub : ∀ {𝕜 : 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 g : E → F}
  {x : E} {s : Set E},
  DifferentiableWithinAt 𝕜 f s x → DifferentiableWithinAt 𝕜 g s x → DifferentiableWithinAt 𝕜 (fun i => f i - g i) s x
-- Mathlib.Algebra.Homology.AlternatingConst
HomologicalComplex.alternatingConst_iCycles_even_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (A : C) {φ ψ : A ⟶ A} (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0)
  (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) {c : ComplexShape ℕ} [inst_2 : DecidableRel c.Rel]
  (hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)) [inst_3 : CategoryTheory.CategoryWithHomology C] {j : ℕ},
  c.Rel (c.prev j) j →
    c.Rel j (c.next j) →
      Even j →
        CategoryTheory.CategoryStruct.comp ((HomologicalComplex.alternatingConst A hOdd hEven hc).iCycles j) φ = 0
-- Mathlib.Algebra.Homology.QuasiIso
ChainComplex.quasiIsoAt₀_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K L : ChainComplex C ℕ} (f : K ⟶ L) [inst_2 : HomologicalComplex.HasHomology K 0]
  [inst_3 : HomologicalComplex.HasHomology L 0] [inst_4 : (HomologicalComplex.sc' K 1 0 0).HasHomology]
  [inst_5 : (HomologicalComplex.sc' L 1 0 0).HasHomology],
  QuasiIsoAt f 0 ↔
    CategoryTheory.ShortComplex.QuasiIso ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.down ℕ) 1 0 0).map f)
-- Mathlib.Condensed.TopComparison
ContinuousMap.yonedaPresheaf.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C TopCat) (Y : Type w')
  [inst_1 : TopologicalSpace Y],
  ContinuousMap.yonedaPresheaf F Y =
    { obj := fun X => C(↑(F.obj (Opposite.unop X)), Y),
      map := fun {X Y_1} f => TypeCat.ofHom fun g => g.comp (TopCat.Hom.hom (F.map f.unop)), map_id := ⋯,
      map_comp := ⋯ }
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.support_conj : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {σ τ : Equiv.Perm α},
  (σ * τ * σ⁻¹).support = Finset.map (Equiv.toEmbedding σ) τ.support
-- Init.Data.Float.Model.Unpacked.Operations.OfNat
/-- Converts an `Int16` to an `UnpackedFloat`, returning positive zero on zero.  -/
Float.Model.UnpackedFloat.ofInt16 : Float.Model.Format → Int16 → Float.Model.UnpackedFloat
-- Mathlib.RepresentationTheory.Intertwining
Representation.Equiv.toIntertwiningMap_trans : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : AddCommMonoid U] [inst_5 : Module A V]
  [inst_6 : Module A W] [inst_7 : Module A U] {ρ : Representation A G V} {σ : Representation A G W}
  {τ : Representation A G U} (φ : ρ.Equiv σ) (ψ : σ.Equiv τ), ↑(φ.trans ψ) = (↑ψ).comp ↑φ
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.tensorHom_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {X₁ X₂ Y₁ Y₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)
      (CategoryTheory.SemiCartesianMonoidalCategory.fst X₂ Y₂) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst X₁ Y₁) f
-- Mathlib.Algebra.Group.Submonoid.Basic
/-- `closure` forms a Galois insertion with the coercion to set.  -/
Submonoid.gi : (M : Type u_1) → [inst : MulOneClass M] → GaloisInsertion Submonoid.closure SetLike.coe
-- Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence
Mathlib.Tactic.Monoidal.naturality_whiskerRight : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {p f g h pf pfh : C} {η : f ≅ g} (η_f : CategoryTheory.MonoidalCategoryStruct.tensorObj p f ≅ pf)
  (η_g : CategoryTheory.MonoidalCategoryStruct.tensorObj p g ≅ pf)
  (η_fh : CategoryTheory.MonoidalCategoryStruct.tensorObj pf h ≅ pfh),
  CategoryTheory.MonoidalCategory.whiskerLeftIso p η ≪≫ η_g = η_f →
    CategoryTheory.MonoidalCategory.whiskerLeftIso p (CategoryTheory.MonoidalCategory.whiskerRightIso η h) ≪≫
        Mathlib.Tactic.Monoidal.normalizeIsoComp η_g η_fh =
      Mathlib.Tactic.Monoidal.normalizeIsoComp η_f η_fh
-- Mathlib.Topology.Maps.Proper.Basic
/-- If `Y` is a compact topological space, then `Prod.fst : X × Y → X` is a proper map.  -/
isProperMap_fst_of_compactSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [CompactSpace Y],
  IsProperMap Prod.fst
-- Mathlib.Topology.Baire.Lemmas
dense_of_mem_residual : ∀ {X : Type u_1} [inst : TopologicalSpace X] [BaireSpace X] {s : Set X}, s ∈ residual X → Dense s
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.Iio_mul_Iic_subset' : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : PartialOrder α] [MulLeftStrictMono α] [MulRightStrictMono α] (a b : α),
  Set.Iio a * Set.Iic b ⊆ Set.Iio (a * b)
-- Mathlib.Data.Multiset.Count
Multiset.count_le_card : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Multiset α), Multiset.count a s ≤ s.card
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.map_sup_comap_of_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {f : M →ₙ* N},
  Function.Surjective ⇑f →
    ∀ (S T : Subsemigroup N), Subsemigroup.map f (Subsemigroup.comap f S ⊔ Subsemigroup.comap f T) = S ⊔ T
-- Mathlib.Topology.Category.TopCat.Monoidal
TopCat.instBraidedCategory : CategoryTheory.BraidedCategory TopCat
-- Mathlib.Algebra.CharZero.Defs
Nat.cast_add_one_ne_zero : ∀ {R : Type u_1} [inst : AddMonoidWithOne R] [CharZero R] (n : ℕ), ↑n + 1 ≠ 0
-- Mathlib.Algebra.Lie.OfAssociative
LieModule.ext_of_isFaithful : ∀ {R : Type u} {L : Type v} (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [LieModule.IsFaithful R L M] {x y : L}, (∀ (m : M), ⁅x, m⁆ = ⁅y, m⁆) → x = y
-- Mathlib.Analysis.Meromorphic.Order
/-- When seen as meromorphic functions, analytic functions have nonnegative order.
 -/
AnalyticAt.meromorphicOrderAt_nonneg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜}, AnalyticAt 𝕜 f x → 0 ≤ meromorphicOrderAt f x
-- Init.Data.Iterators.Lemmas.Consumers.Collect
Std.Iter.toList_eq_of_atIdxSlow?_eq : ∀ {α₁ α₂ β : Type u_1} [inst : Std.Iterator α₁ Id β] [Std.Iterators.Finite α₁ Id] [inst_2 : Std.Iterator α₂ Id β]
  [Std.Iterators.Finite α₂ Id] {it₁ : Std.Iter β} {it₂ : Std.Iter β},
  (∀ (k : ℕ), Std.Iter.atIdxSlow? k it₁ = Std.Iter.atIdxSlow? k it₂) → it₁.toList = it₂.toList