mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.iso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} (D : F.DescentData f) ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁)
  (f₂ : Y ⟶ X i₂)
  (_hf₁ :
    autoParam (CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q) CategoryTheory.Pseudofunctor.DescentData.iso._auto_1)
  (_hf₂ :
    autoParam (CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q) CategoryTheory.Pseudofunctor.DescentData.iso._auto_3),
  (D.iso q f₁ f₂ _hf₁ _hf₂).hom = D.hom q f₁ f₂ ⋯ ⋯
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.instNSMul : {α : Type u} →
  {R : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : PseudoMetricSpace R] →
        [inst_2 : AddMonoid R] → [BoundedAdd R] → [ContinuousAdd R] → SMul ℕ (BoundedContinuousFunction α R)
-- Mathlib.Data.List.DropRight
List.rtakeWhile_concat_neg : ∀ {α : Type u_1} (p : α → Bool) (l : List α) (x : α), ¬p x = true → List.rtakeWhile p (l ++ [x]) = []
-- Init.Data.List.MapIdx
List.mapIdx.go.eq_def : ∀ {α : Type u_1} {β : Type u_2} (f : ℕ → α → β) (a : List α) (a_1 : Array β),
  List.mapIdx.go f a a_1 =
    match a, a_1 with
    | [], acc => acc.toList
    | a :: as, acc => List.mapIdx.go f as (acc.push (f acc.size a))
-- Mathlib.Algebra.Module.LinearMap.Index
LinearMap.index_smul : ∀ {M : Type u_1} {N : Type u_2} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] {k : Type u_3} [inst_2 : Field k]
  [inst_3 : Module k M] [inst_4 : Module k N] {f : M →ₗ[k] N} (t : k), t ≠ 0 → (t • f).index = f.index
-- Mathlib.Algebra.Order.ZeroLEOne
/-- `zero_le_one` with the type argument implicit.  -/
zero_le_one : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : One α] [inst_2 : LE α] [ZeroLEOneClass α], 0 ≤ 1
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
IsDiscreteValuationRing.aux_pid_of_ufd_of_unique_irreducible : ∀ (R : Type u) [inst : CommRing R] [UniqueFactorizationMonoid R],
  (∃ p, Irreducible p) → (∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q) → IsPrincipalIdealRing R
-- Mathlib.Data.Set.MemPartition
memPartitionSet_mem : ∀ {α : Type u_1} (f : ℕ → Set α) (n : ℕ) (a : α), memPartitionSet f n a ∈ memPartition f n
-- Batteries.Util.ProofWanted
/-- The binder type, e.g. `ProofWanted.Stmt foo` for parameterless `foo`, or
`∀ (n : Nat), (foo n).Stmt` if `foo` itself has binders.  -/
_private.Batteries.Util.ProofWanted.0.WantedRefInfo.binderType : WantedRefInfo✝ → Lean.TSyntax `term
-- Std.Sat.CNF.Basic
/-- A CNF formula.

Literals are identified by members of `α`.
 -/
Std.Sat.CNF : Type u → Type u
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions
CategoryTheory.LocalizerMorphism.functorialRightResolutions.ι.congr_simp : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂}
  {ρ : CategoryTheory.Functor C₂ C₁} (i i_1 : CategoryTheory.Functor.id C₂ ⟶ ρ.comp Φ.functor),
  i = i_1 →
    ∀ [inst_2 : Φ.functor.Full] [inst_3 : Φ.functor.Faithful],
      CategoryTheory.LocalizerMorphism.functorialRightResolutions.ι i =
        CategoryTheory.LocalizerMorphism.functorialRightResolutions.ι i_1
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.orderIsoEquivIso_symm_apply : ∀ {α β : PartOrdEmb} (e : ↑α ≃o ↑β), PartOrdEmb.orderIsoEquivIso.symm e = PartOrdEmb.Iso.mk e
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.entryAtIdxD_eq_getD_entryAtIdx? : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β} {i : ℕ} {fallback : (a : α) × β a},
  t.entryAtIdxD i fallback = (t.entryAtIdx? i).getD fallback
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.constGetEntryLE_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) {k : α} {he : ∃ a ∈ t₁, (compare a k).isLE = true},
  Std.DTreeMap.Internal.Impl.Const.getEntryLE k t₁ ⋯ he = Std.DTreeMap.Internal.Impl.Const.getEntryLE k t₂ ⋯ ⋯
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.zero_mem : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (L' : LieSubalgebra R L),
  0 ∈ L'
-- Mathlib.Data.Set.Monotone
StrictMonoOn.congr : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ : α → β} [inst : Preorder α] [inst_1 : Preorder β],
  StrictMonoOn f₁ s → Set.EqOn f₁ f₂ s → StrictMonoOn f₂ s
-- Std.Sync.Broadcast
Std.instToStringBroadcastError : ToString Std.Broadcast.Error
-- Mathlib.Topology.DenseEmbedding
/-- The dense embedding of a subtype inside its closure.  -/
IsDenseEmbedding.subtypeEmb : {β : Type u_2} →
  [inst : TopologicalSpace β] →
    {α : Type u_5} → (p : α → Prop) → (e : α → β) → { x // p x } → { x // x ∈ closure (e '' {x | p x}) }
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.size_rcc : ∀ {a b : ℕ}, (a...=b).size = b + 1 - a
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.instIsScalarTower : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {R : Type u_2}
  [inst_2 : Semiring R] [inst_3 : NonUnitalNonAssocSemiring β] [inst_4 : IsTopologicalSemiring β] [inst_5 : Module R β]
  [inst_6 : ContinuousConstSMul R β] [IsScalarTower R β β],
  IsScalarTower R (ZeroAtInftyContinuousMap α β) (ZeroAtInftyContinuousMap α β)
-- Mathlib.Topology.Compactification.StoneCech
Ultrafilter.t2Space : ∀ {α : Type u}, T2Space (Ultrafilter α)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_insertMany!_list_of_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {l : List ((a : α) × β a)} {k k' fallback : α},
      compare k k' = Ordering.eq →
        List.Pairwise (fun a b => ¬compare a.fst b.fst = Ordering.eq) l →
          k ∈ List.map Sigma.fst l → (↑(t.insertMany! l)).getKeyD k' fallback = k
-- Lean.DocString.Markdown
_private.Lean.DocString.Markdown.0.Lean.Doc.trimRight.go : {i : Type u_1} → Array (Lean.Doc.Inline i) → Lean.Doc.Inline i × String
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.trans : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  (x y z : RingCat.Colimits.Prequotient F),
  RingCat.Colimits.Relation F x y → RingCat.Colimits.Relation F y z → RingCat.Colimits.Relation F x z
-- Mathlib.Analysis.LocallyConvex.Basic
Balanced.neg : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {s : Set E},
  Balanced 𝕜 s → Balanced 𝕜 (-s)
-- Mathlib.Algebra.Group.Action.Defs
/-- Pullback an additive action along an injective map respecting `+ᵥ`.  -/
Function.Injective.addAction : {M : Type u_1} →
  {α : Type u_5} →
    {β : Type u_6} →
      [inst : AddMonoid M] →
        [inst_1 : AddAction M α] →
          [inst_2 : VAdd M β] →
            (f : β → α) → Function.Injective f → (∀ (c : M) (x : β), f (c +ᵥ x) = c +ᵥ f x) → AddAction M β
-- Init.Omega.Int
_private.Init.Omega.Int.0.Int.neg.match_1.splitter : (motive : ℤ → Sort u_1) → (n : ℤ) → ((n : ℕ) → motive (Int.ofNat n)) → ((n : ℕ) → motive (Int.negSucc n)) → motive n
-- Mathlib.Geometry.Manifold.HasGroupoid
/-- If `G` is closed under restriction, the transition function between the restriction of two
charts `e` and `e'` lies in `G`.  -/
StructureGroupoid.trans_restricted : ∀ {H : Type u} {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  {e e' : OpenPartialHomeomorph M H} {G : StructureGroupoid H},
  e ∈ atlas H M →
    e' ∈ atlas H M →
      ∀ [HasGroupoid M G] [ClosedUnderRestriction G] {s : TopologicalSpace.Opens M} (hs : Nonempty ↥s),
        (e.subtypeRestr hs).symm.trans (e'.subtypeRestr hs) ∈ G
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.Arrow.cechNerve_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow C)
  [inst_1 : ∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom]
  (n : SimplexCategoryᵒᵖ),
  f.cechNerve.obj n = CategoryTheory.Limits.widePullback f.right (fun x => f.left) fun x => f.hom
-- Mathlib.NumberTheory.ModularForms.CuspFormSubmodule
/-- The inclusion of cusp forms into modular forms, as a ℂ-linear map.  -/
CuspForm.toModularFormₗ : {Γ : Subgroup (GL (Fin 2) ℝ)} → {k : ℤ} → [inst : Γ.HasDetOne] → CuspForm Γ k →ₗ[ℂ] ModularForm Γ k
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
IsUniformAddGroup.uniformity_countably_generated : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] [(nhds 0).IsCountablyGenerated],
  (uniformity α).IsCountablyGenerated
-- Mathlib.Tactic.NormNum.Ineq
Mathlib.Meta.NormNum.isNNRat_le_false : ∀ {α : Type u_1} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a b : α} {na nb da db : ℕ},
  Mathlib.Meta.NormNum.IsNNRat a na da →
    Mathlib.Meta.NormNum.IsNNRat b nb db → decide (nb * da < na * db) = true → ¬a ≤ b
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.denote_combine' : ∀ (ctx : Int.Internal.Linear.Context) (fuel : ℕ) (p₁ p₂ : Int.Internal.Linear.Poly),
  Int.Internal.Linear.Poly.denote ctx (Int.Internal.Linear.Poly.combine' fuel p₁ p₂) =
    Int.Internal.Linear.Poly.denote ctx p₁ + Int.Internal.Linear.Poly.denote ctx p₂
-- Mathlib.Analysis.Normed.Group.AddTorsor
nndist_vsub_cancel_left : ∀ {V : Type u_2} {P : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] (x y z : P), nndist (x -ᵥ y) (x -ᵥ z) = nndist y z
-- Mathlib.Topology.Clopen
IsClopen.inter : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsClopen s → IsClopen t → IsClopen (s ∩ t)
-- Mathlib.Topology.Order.Basic
/-- If a topology is generated by half-open intervals with endpoints in a set `c`, then the sets
formed by intersecting finitely many of these intervals form a topological basis.  -/
isTopologicalBasis_biInter_Ioi_Iio_of_generateFrom : ∀ {α : Type u} [ts : TopologicalSpace α] [inst : Preorder α] (c : Set α),
  ts = TopologicalSpace.generateFrom {s | ∃ a ∈ c, s = Set.Ioi a ∨ s = Set.Iio a} →
    TopologicalSpace.IsTopologicalBasis
      {s | ∃ f g, f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Set.Ioi a) ∩ ⋂ a ∈ g, Set.Iio a}
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.strictAntiOn_one_add_smoothingFn : StrictAntiOn (fun x => 1 + AkraBazziRecurrence.smoothingFn x) (Set.Ioi 1)
-- Mathlib.Data.Finset.Basic
Finset.isDirected_subset : ∀ {α : Type u_1}, IsDirected (Finset α) fun x1 x2 => x1 ⊆ x2
-- Init.System.Platform
/-- The LLVM target triple of the current platform. Empty if missing when Lean was compiled.
 -/
System.Platform.target : String
-- Mathlib.Algebra.Homology.DifferentialObject
CategoryTheory.DifferentialObject.objEqToHom.congr_simp : ∀ {β : Type u_1} [inst : AddCommGroup β] {b : β} {V : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_2} V]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V]
  (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) {i j : β} (h : i = j),
  X.objEqToHom h = X.objEqToHom h
-- Mathlib.Analysis.Complex.Basic
Complex.reCLM_coe : ↑Complex.reCLM = Complex.reLm
-- Lean.Parser.Term
Lean.Parser.Command.commentBody.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.SInt.Lemmas
Int16.not_lt_minValue : ∀ {a : Int16}, ¬a < Int16.minValue
-- Aesop.Forward.LevelIndex
Aesop.instOrdLevelIndex : Ord Aesop.LevelIndex
-- Mathlib.Topology.Convenient.GeneratedBy
Topology.IsGeneratedBy.isOpen_iff : ∀ {ι : Type t} (X : ι → Type u) [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y]
  [Topology.IsGeneratedBy X Y] {U : Set Y}, IsOpen U ↔ ∀ ⦃i : ι⦄ (f : C(X i, Y)), IsOpen (⇑f ⁻¹' U)
-- Mathlib.Analysis.InnerProductSpace.Laplacian
/-- The Laplacian commutes with addition.  -/
ContDiffAt.laplacian_add : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f₁ f₂ : E → F} {x : E},
  ContDiffAt ℝ 2 f₁ x →
    ContDiffAt ℝ 2 f₂ x → Laplacian.laplacian (f₁ + f₂) x = Laplacian.laplacian f₁ x + Laplacian.laplacian f₂ x
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.ext_getKey_getElem? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {t₁ t₂ : Std.ExtTreeMap α β cmp},
  (∀ (k : α) (hk : k ∈ t₁) (hk' : k ∈ t₂), t₁.getKey k hk = t₂.getKey k hk') → (∀ (k : α), t₁[k]? = t₂[k]?) → t₁ = t₂
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.congrIndexOneOfEq.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {i i' j j' : E.I₀} (hii' : i = i') (hjj' : j = j'),
  CategoryTheory.PreOneHypercover.congrIndexOneOfEq hii' hjj' = hii' ▸ hjj' ▸ Equiv.refl (E.I₁ i j)
-- Mathlib.Topology.Inseparable
inseparable_iff_forall_isClosed : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, Inseparable x y ↔ ∀ (s : Set X), IsClosed s → (x ∈ s ↔ y ∈ s)
-- Lean.Elab.Syntax
Lean.Elab.Command.strLitToPattern : Lean.Syntax → Lean.MacroM Lean.Syntax
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Set.Finite.toFinset_add : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α] {s t : Set α} (hs : s.Finite) (ht : t.Finite)
  (hf : optParam (s + t).Finite ⋯), hf.toFinset = hs.toFinset + ht.toFinset
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.GeneratorNode.currInstanceIdx : Lean.Meta.SynthInstance.GeneratorNode → ℕ
-- Mathlib.Algebra.Pointwise.Stabilizer
MulAction.stabilizer_inf_stabilizer_le_stabilizer_inter : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] {s t : Set α},
  MulAction.stabilizer G s ⊓ MulAction.stabilizer G t ≤ MulAction.stabilizer G (s ∩ t)
-- Mathlib.Analysis.RCLike.Basic
RCLike.toIsOrderedAddMonoid : ∀ {K : Type u_1} [inst : RCLike K], IsOrderedAddMonoid K
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.prod_range_succ : ∀ {M : Type u_4} [inst : Monoid M] (f : ℕ → M) (n : ℕ),
  (List.map f (List.range n.succ)).prod = (List.map f (List.range n)).prod * f n
-- Mathlib.AlgebraicGeometry.Morphisms.Integral
AlgebraicGeometry.IsIntegralHom.instIsMultiplicativeScheme : CategoryTheory.MorphismProperty.IsMultiplicative @AlgebraicGeometry.IsIntegralHom
-- Mathlib.Algebra.Order.Interval.Set.Group
Set.sub_mem_Ico_zero_iff_right : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {a b : α},
  b - a ∈ Set.Ico 0 b ↔ a ∈ Set.Ioc 0 b
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.IsAcyclic.eq_1 : ∀ {V : Type u_1} (G : SimpleGraph V), G.IsAcyclic = ∀ ⦃v : V⦄ (c : G.Walk v v), ¬c.IsCycle
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.ker_eq_top_iff : ∀ {G : Type u_1} [inst : Group G] {M : Type u_7} [inst_1 : MulOneClass M] {f : G →* M}, f.ker = ⊤ ↔ f = 1
-- Mathlib.Topology.Inseparable
specializes_rfl : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x : X}, x ⤳ x
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- commutation with `g'`  -/
CategoryTheory.ShortComplex.RightHomologyMapData.commg'_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData}
  (self : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) {Z : C} (h : S₂.X₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.φQ (CategoryTheory.CategoryStruct.comp h₂.g' h) =
    CategoryTheory.CategoryStruct.comp h₁.g' (CategoryTheory.CategoryStruct.comp φ.τ₃ h)
-- Mathlib.Analysis.SpecificLimits.Normed
summable_of_ratio_test_tendsto_lt_one : ∀ {α : Type u_4} [inst : NormedAddCommGroup α] [CompleteSpace α] {f : ℕ → α} {l : ℝ},
  l < 1 →
    (∀ᶠ (n : ℕ) in Filter.atTop, f n ≠ 0) →
      Filter.Tendsto (fun n => ‖f (n + 1)‖ / ‖f n‖) Filter.atTop (nhds l) → Summable f
-- Std.Http.Internal.Char
/-- Checks if a byte is an alphabetic character (a-z or A-Z).
 -/
Std.Http.Internal.Char.isAlphaByte : UInt8 → Bool
-- Mathlib.Order.Interval.Finset.Basic
Finset.notMem_Iio_self : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrderBot α] {b : α}, b ∉ Finset.Iio b
-- Mathlib.CategoryTheory.EffectiveEpi.Preserves
/-- Equivalences preserve effective epimorphic families  -/
CategoryTheory.effectiveEpiFamilyStructOfEquivalence : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (e : C ≌ D) →
          {B : C} →
            {α : Type u_3} →
              (X : α → C) →
                (π : (a : α) → X a ⟶ B) →
                  [CategoryTheory.EffectiveEpiFamily X π] →
                    CategoryTheory.EffectiveEpiFamilyStruct (fun a => e.functor.obj (X a)) fun a => e.functor.map (π a)
-- Mathlib.Data.Sym.Basic
Sym.mem_attach : ∀ {α : Type u_1} {n : ℕ} (s : Sym α n) (x : { x // x ∈ s }), x ∈ s.attach
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
mem_skewAdjointMatricesSubmodule' : ∀ {R₂ : Type u_3} [inst : CommRing R₂] {n : Type u_5} [inst_1 : Fintype n] (J A : Matrix n n R₂)
  [inst_2 : DecidableEq n], A ∈ skewAdjointMatricesSubmodule J ↔ J.IsSkewAdjoint A
-- Mathlib.Data.ENNReal.BigOperators
ENNReal.prod_div_distrib_of_ne_top : ∀ {ι : Type u_1} {f g : ι → ENNReal} {s : Finset ι},
  (∀ i ∈ s, g i ≠ ⊤) → ∏ i ∈ s, f i / g i = (∏ i ∈ s, f i) / ∏ i ∈ s, g i
-- Mathlib.Topology.Connected.Basic
/-- Theorem of bark and tree: if a set is within a connected set and its closure, then it is
connected as well. See also `IsPreconnected.subset_closure`.  -/
IsConnected.subset_closure : ∀ {α : Type u} [inst : TopologicalSpace α] {s t : Set α}, IsConnected s → s ⊆ t → t ⊆ closure s → IsConnected t
-- Mathlib.Tactic.TryThis
/-- Produces the text `Try this: <tac>` with the given conv tactic, and then executes it.  -/
Mathlib.Tactic.convTry_this__ : Lean.ParserDescr
-- Mathlib.Order.Minimal
Minimal.eq_of_subset : ∀ {α : Type u_2} {P : Set α → Prop} {s t : Set α}, Minimal P s → P t → t ⊆ s → t = s
-- Lean.Parser.Module
Lean.Parser.ModuleParserState.mk.inj : ∀ {pos : String.Pos.Raw} {recovering hasLeading : Bool} {pos_1 : String.Pos.Raw} {recovering_1 hasLeading_1 : Bool},
  { pos := pos, recovering := recovering, hasLeading := hasLeading } =
      { pos := pos_1, recovering := recovering_1, hasLeading := hasLeading_1 } →
    pos = pos_1 ∧ recovering = recovering_1 ∧ hasLeading = hasLeading_1
-- Mathlib.RingTheory.LocalIso
Algebra.IsLocalIso.pi_of_finite : ∀ {ι : Type u_3} (R : Type u_4) (S : ι → Type u_5) [inst : CommSemiring R] [inst_1 : (i : ι) → CommRing (S i)]
  [inst_2 : (i : ι) → Algebra R (S i)] [Finite ι] [∀ (i : ι), Algebra.IsLocalIso R (S i)],
  Algebra.IsLocalIso R ((i : ι) → S i)
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Matrix.isNilpotent_charpoly_sub_pow_of_isNilpotent : ∀ {R : Type u} [inst : CommRing R] {n : Type v} [inst_1 : DecidableEq n] [inst_2 : Fintype n] {M : Matrix n n R},
  IsNilpotent M → IsNilpotent (M.charpoly - Polynomial.X ^ Fintype.card n)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.mkIso'_inv_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G H : C} (e : G ≅ H) [inst_2 : CategoryTheory.AddGrpObj G] [inst_3 : CategoryTheory.AddGrpObj H]
  [inst_4 : CategoryTheory.IsAddMonHom e.hom], (CategoryTheory.AddGrp.mkIso' e).inv.hom.hom = e.inv
-- Init.Data.SInt.Lemmas
ISize.maxValue_le_iff : ∀ {a : ISize}, ISize.maxValue ≤ a ↔ a = ISize.maxValue
-- Mathlib.GroupTheory.NoncommCoprod
MonoidHom.noncommCoprod_unique : ∀ {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 × N →* P), (f.comp (MonoidHom.inl M N)).noncommCoprod (f.comp (MonoidHom.inr M N)) ⋯ = f
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.pow_mk : ∀ {α : Type u} {L : List (α × Bool)} (n : ℕ), FreeGroup.mk L ^ n = FreeGroup.mk (List.replicate n L).flatten
-- Lean.Meta.Tactic.TryThis
/-- Add a list of "try this" suggestions as a single "try these" suggestion. This has two effects:

* A widget diagnostic is displayed, saying `Try these: <list of suggestions>` with a link on
  each suggestion in `<list of suggestions>` to apply each suggestion
* A code action for each suggestion is added, which will apply the suggestion.

The parameters are:
* `ref`: the span of the widget diagnostic
* `suggestions`: an array of `Suggestion`s, which each contain
  * `suggestion`: the replacement text
  * `preInfo?`: an optional string shown immediately before the replacement text in the widget
    message (only)
  * `postInfo?`: an optional string shown immediately after the replacement text in the widget
    message (only)
  * `messageData?`: an optional `MessageData` displayed instead of `suggestion`.
    If set, implies `diffGranularity = .none`.
  * `toCodeActionTitle?`: an optional function `String → String` describing how to transform the
    pretty-printed suggestion text into the code action text which appears in the lightbulb menu.
    If `none`, we simply prepend `"Try this: "` to the suggestion text.
* `origSpan?`: a syntax object whose span is the actual text to be replaced by `suggestion`.
  If not provided it defaults to `ref`.
* `header`: a string that precedes the list. By default, it is `"Try these:"`.
* `style?` (**deprecated**): unused.
* `codeActionPrefix?`: an optional string to be used as the prefix of the replacement text for all
  suggestions which do not have a custom `toCodeActionTitle?`. If not provided, `"Try this: "` is
  used.
* `diffGranularity`: How to compute the diff display in the suggestion. Defaults to only displaying
  the inserted string.
 -/
Lean.Meta.Tactic.TryThis.addSuggestions : Lean.Syntax →
  Array Lean.Meta.Tactic.TryThis.Suggestion →
    optParam (Option Lean.Syntax) none →
      optParam String "Try these:" →
        optParam (Option Lean.Meta.Tactic.TryThis.SuggestionStyle) none →
          optParam (Option String) none →
            optParam Lean.Meta.Hint.DiffGranularity Lean.Meta.Hint.DiffGranularity.none →
              optParam Lean.MessageData Lean.MessageData.nil → Lean.CoreM Unit
-- Mathlib.NumberTheory.ArithmeticFunction.Moebius
ArithmeticFunction.IsMultiplicative.prodPrimeFactors_one_sub_of_squarefree : ∀ {R : Type u_1} [inst : CommRing R] (f : ArithmeticFunction R),
  f.IsMultiplicative →
    ∀ {n : ℕ}, Squarefree n → ∏ p ∈ n.primeFactors, (1 - f p) = ∑ d ∈ n.divisors, ↑(ArithmeticFunction.moebius d) * f d
-- Mathlib.Algebra.GroupWithZero.Units.Basic
div_eq_iff : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a b c : G₀}, b ≠ 0 → (a / b = c ↔ a = c * b)
-- Mathlib.GroupTheory.HNNExtension
/-- A condition for not cancelling whose hypotheses are the same as those of the `cons` function.  -/
HNNExtension.NormalWord.not_cancels_of_cons_hyp : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B} (u : ℤˣ)
  (w : HNNExtension.NormalWord d),
  (∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ HNNExtension.toSubgroup A B u → u = u') →
    ¬HNNExtension.NormalWord.Cancels u w
-- Mathlib.AlgebraicTopology.SimplicialSet.Nerve
CategoryTheory.nerve.δ₂_mk₂_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₀ X₁ X₂ : C} (f : X₀ ⟶ X₁) (g : X₁ ⟶ X₂),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (CategoryTheory.nerve C) 2))
      (CategoryTheory.ComposableArrows.mk₂ f g) =
    CategoryTheory.ComposableArrows.mk₁ f