mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- **Alias** of `mul_apply_eq_comp`. -/
ContinuousLinearMap.mul_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {inst : FunLike F α α} {inst_1 : Mul F} [self : IsMulApplyEqComp F α]
  (f g : F) (x : α), (f * g) x = f (g x)
-- Init.Data.List.Monadic
List.zipWithM'.match_1.congr_eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : List α → List β → Sort u_3) (x : List α) (x_1 : List β)
  (h_1 : (x : α) → (xs : List α) → (y : β) → (ys : List β) → motive (x :: xs) (y :: ys))
  (h_2 : (x : List α) → (x_2 : List β) → motive x x_2) (x_2 : α) (xs : List α) (y : β) (ys : List β),
  x = x_2 :: xs →
    x_1 = y :: ys →
      (match x, x_1 with
        | x :: xs, y :: ys => h_1 x xs y ys
        | x, x_3 => h_2 x x_3) ≍
        h_1 x_2 xs y ys
-- Mathlib.Algebra.Algebra.Pi
AlgEquiv.funUnique_symm_apply : ∀ {R : Type u_3} {ι : Type u_4} [inst : CommSemiring R] (S : Type u_8) [inst_1 : Semiring S] [inst_2 : Algebra R S]
  [inst_3 : Unique ι] (x : S), (AlgEquiv.funUnique R ι S).symm x = (Equiv.funUnique ι S).symm x
-- Mathlib.Order.Hom.Basic
OrderHom.dual_symm_apply_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : αᵒᵈ →o βᵒᵈ) (a : α),
  (OrderHom.dual.symm f) a = (⇑OrderDual.ofDual ∘ ⇑f ∘ ⇑OrderDual.toDual) a
-- Mathlib.GroupTheory.GroupAction.Jordan
/-- Jordan's multiple primitivity criterion (Wielandt, 13.3)  -/
MulAction.IsPreprimitive.isMultiplyPreprimitive : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
  MulAction.IsPreprimitive G α →
    ∀ {s : Set α} {n : ℕ},
      s.ncard = n + 1 →
        n + 2 < Nat.card α →
          MulAction.IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) →
            MulAction.IsMultiplyPreprimitive G α (n + 2)
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.OldCollector.collect : Lean.Expr → Lean.Meta.Grind.CollectorM✝ Unit
-- Mathlib.Combinatorics.SimpleGraph.CycleGraph
SimpleGraph.cycleGraph_two_eq_top : SimpleGraph.cycleGraph 2 = ⊤
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- Two sets are at zero Hausdorff distance if and only if they have the same closures.  -/
Metric.hausdorffDist_zero_iff_closure_eq_closure : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s t : Set α},
  Metric.hausdorffEDist s t ≠ ⊤ → (Metric.hausdorffDist s t = 0 ↔ closure s = closure t)
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.algebraMap_X_pow : ∀ {R : Type u_1} [inst : CommSemiring R] (n : ℕ),
  (algebraMap (Polynomial R) (LaurentPolynomial R)) (Polynomial.X ^ n) = LaurentPolynomial.T ↑n
-- Mathlib.Order.Antichain
setOfPred_minimal_antichain : ∀ {α : Type u_1} [inst : PartialOrder α] (P : α → Prop), IsAntichain (fun x1 x2 => x1 ≤ x2) {x | Minimal P x}
-- Lean.Meta.Tactic.Cases
Lean.Meta.ByCasesSubgoal.mk.inj : ∀ {mvarId : Lean.MVarId} {fvarId : Lean.FVarId} {mvarId_1 : Lean.MVarId} {fvarId_1 : Lean.FVarId},
  { mvarId := mvarId, fvarId := fvarId } = { mvarId := mvarId_1, fvarId := fvarId_1 } →
    mvarId = mvarId_1 ∧ fvarId = fvarId_1
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.piFinTwo_apply : ∀ (α : Fin 2 → Type u) [inst : (i : Fin 2) → UniformSpace (α i)], ⇑(UniformEquiv.piFinTwo α) = fun f => (f 0, f 1)
-- Lean.Elab.ParseImportsFast
Lean.ParseImports.setIsModule : Bool → Lean.ParseImports.Parser
-- Lean.Data.Json.Printer
_private.Lean.Data.Json.Printer.0.Lean.Json.CompressWorkItemQueue.pushObjectFieldKey : Lean.Json.CompressWorkItemQueue✝ → String → Lean.Json.CompressWorkItemQueue✝
-- Mathlib.Order.Disjoint
/-- **Alias** of `symm_codisjoint`. -/
symmetric_codisjoint : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderTop α], Std.Symm Codisjoint
-- Std.Data.DHashMap.Internal.Model
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.get!ₘ : {α : Type u} →
  {β : α → Type v} →
    [inst : BEq α] → [LawfulBEq α] → [Hashable α] → Std.DHashMap.Internal.Raw₀ α β → (a : α) → [Inhabited (β a)] → β a
-- Lean.Elab.DeprecatedArg
/-- Look up a deprecated argument mapping for `(declName, argName)`.  -/
Lean.Elab.findDeprecatedArg? : Lean.Environment → Lean.Name → Lean.Name → Option Lean.Elab.DeprecatedArgEntry
-- Mathlib.Order.Category.BoolAlg
BoolAlg.instConcreteCategoryBoundedLatticeHomCarrier : CategoryTheory.ConcreteCategory BoolAlg fun x1 x2 => BoundedLatticeHom ↑x1 ↑x2
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get_insert!_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {v : β}, Std.DTreeMap.Internal.Impl.Const.get (Std.DTreeMap.Internal.Impl.insert! k v t) k ⋯ = v
-- Mathlib.Algebra.Category.MonCat.Limits
/-- The category of monoids has all limits.  -/
MonCat.hasLimitsOfSize : ∀ [UnivLE.{v, u}], CategoryTheory.Limits.HasLimitsOfSize.{w, v, u, u + 1} MonCat
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.SimpleFunc.memLp_of_finite_measure_preimage : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {μ : MeasureTheory.Measure α}
  (p : ENNReal) {f : MeasureTheory.SimpleFunc α E},
  (∀ (y : E), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤) → MeasureTheory.MemLp (⇑f) p μ
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.modify : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α], m₁.WF → m₂.WF → ∀ (k : α) (f : β k → β k), m₁.Equiv m₂ → (m₁.modify k f).Equiv (m₂.modify k f)
-- Mathlib.Data.Nat.Choose.Basic
Nat.choose_eq_factorial_div_factorial : ∀ {n k : ℕ}, k ≤ n → n.choose k = n.factorial / (k.factorial * (n - k).factorial)
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
AlgebraicIndependent.cardinalMk_le_trdeg : ∀ {R : Type u_2} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] [Nontrivial R]
  {ι : Type v} {x : ι → A}, AlgebraicIndependent R x → Cardinal.mk ι ≤ Algebra.trdeg R A
-- Mathlib.Algebra.Group.Subsemigroup.Defs
MulMemClass.coe_mul : ∀ {M : Type u_1} {A : Type u_3} [inst : Mul M] [inst_1 : SetLike A M] [hA : MulMemClass A M] (S' : A) (x y : ↥S'),
  ↑(x * y) = ↑x * ↑y
-- Plausible.Random
/-- Run the random computation `cmd` with `seed` for the RNG.
 -/
Plausible.runRandWith : {m : Type → Type u_1} → [Monad m] → {α : Type} → ℕ → Plausible.RandT m α → m α
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
/-- A functor `F` is additive provided `F.map` is an additive homomorphism.  -/
CategoryTheory.Functor.Additive : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [CategoryTheory.Preadditive C] → [CategoryTheory.Preadditive D] → CategoryTheory.Functor C D → Prop
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- A composition of natural transformations gives the composition of corresponding functors.  -/
CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransComp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F₀ F₁ F₂ : CategoryTheory.Functor C C} →
      (α : F₀ ⟶ F₁) →
        (β : F₁ ⟶ F₂) →
          CategoryTheory.Endofunctor.Coalgebra.functorOfNatTrans (CategoryTheory.CategoryStruct.comp α β) ≅
            (CategoryTheory.Endofunctor.Coalgebra.functorOfNatTrans α).comp
              (CategoryTheory.Endofunctor.Coalgebra.functorOfNatTrans β)
-- Mathlib.Data.EReal.Basic
EReal.mul_comm : ∀ (x y : EReal), x * y = y * x
-- Mathlib.Data.Quot
Trunc.induction_on₂ : ∀ {α : Sort u_1} {β : Sort u_2} {C : Trunc α → Trunc β → Prop} (q₁ : Trunc α) (q₂ : Trunc β),
  (∀ (a : α) (b : β), C (Trunc.mk a) (Trunc.mk b)) → C q₁ q₂
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.leibnizPullback_map_app : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  (G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)) [inst_3 : CategoryTheory.Limits.HasPullbacks C₂]
  {X Y : (CategoryTheory.Arrow C₁)ᵒᵖ} (sq : X ⟶ Y) (f₃ : CategoryTheory.Arrow C₃),
  (G.leibnizPullback.map sq).app f₃ =
    (CategoryTheory.Functor.PullbackObjObj.ofHasPullback G (Opposite.unop X).hom f₃.hom).mapArrowLeft
      (CategoryTheory.Functor.PullbackObjObj.ofHasPullback G (Opposite.unop Y).hom f₃.hom) sq.unop
-- Mathlib.Data.Fin.Tuple.Basic
/-- Variant of `append_left` using `Fin.castLE` instead of `Fin.castAdd`.  -/
Fin.append_left' : ∀ {m n : ℕ} {α : Sort u_1} (u : Fin m → α) (v : Fin n → α) (i : Fin m), Fin.append u v (Fin.castLE ⋯ i) = u i
-- Mathlib.NumberTheory.Ostrowski
_private.Mathlib.NumberTheory.Ostrowski.0.list_geom : ∀ {T : Type u_1} {F : Type u_2} [inst : DivisionRing F] (l : List T) {y : F},
  y ≠ 1 → (List.mapIdx (fun i x => y ^ i) l).sum = (y ^ l.length - 1) / (y - 1)
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.IsMultiplicative.map_prod_of_subset_primeFactors : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {f : ArithmeticFunction R},
  f.IsMultiplicative → ∀ (l : ℕ), ∀ t ⊆ l.primeFactors, f (∏ a ∈ t, a) = ∏ a ∈ t, f a
-- Mathlib.Tactic.CategoryTheory.Coherence
Mathlib.Tactic.Coherence.LiftHom.comp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      [inst_1 : Mathlib.Tactic.Coherence.LiftObj X] →
        [inst_2 : Mathlib.Tactic.Coherence.LiftObj Y] →
          [inst_3 : Mathlib.Tactic.Coherence.LiftObj Z] →
            (f : X ⟶ Y) →
              (g : Y ⟶ Z) →
                [Mathlib.Tactic.Coherence.LiftHom f] →
                  [Mathlib.Tactic.Coherence.LiftHom g] →
                    Mathlib.Tactic.Coherence.LiftHom (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.coe_nnreal_smul : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (c : NNReal) (μ : MeasureTheory.Measure α), ↑c • μ = c • μ
-- Lean.Compiler.NameMangling
_private.Lean.Compiler.NameMangling.0.Lean.Name.demangleAux.match_6.eq_1 : ∀ (s : String) (motive : Char → Option (s.Pos × ℕ) → Sort u_1) (q : s.Pos) (v : ℕ)
  (h_1 : (q_1 : s.Pos) → (v_1 : ℕ) → some (q, v) = some (q_1, v_1) → motive 'x' (some (q_1, v_1)))
  (h_2 : (x : Char) → (x_1 : Option (s.Pos × ℕ)) → some (q, v) = x_1 → motive x x_1),
  (match 'x', h₁ : some (q, v) with
    | 'x', some (q_1, v_1) => h_1 q_1 v_1 h₁
    | x, x_1 => h_2 x x_1 h₁) =
    h_1 q v ⋯
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.foldl_filterMap'.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : (b : β) → motive (some b)) (h_2 : Unit → motive none),
  (match none with
    | some b => h_1 b
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.LinearAlgebra.Matrix.Trace
Matrix.trace_mul_cycle : ∀ {m : Type u_2} {n : Type u_3} {p : Type u_4} {R : Type u_6} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : Fintype p] [inst_3 : NonUnitalCommSemiring R] (A : Matrix m n R) (B : Matrix n p R) (C : Matrix p m R),
  (A * B * C).trace = (C * A * B).trace
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.liftAlgHom_injective : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] {L : Type u_1} {S : Type u_3} [inst_2 : Field L]
  [inst_3 : CommSemiring S] [inst_4 : Algebra S (Polynomial K)] [inst_5 : Algebra S L] (φ : Polynomial K →ₐ[S] L)
  (hφ : Function.Injective ⇑φ)
  (hφ' : optParam (nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L)) ⋯),
  Function.Injective ⇑(RatFunc.liftAlgHom φ hφ')
-- Mathlib.Topology.Algebra.Module.ModuleTopology
/-- If `R` is a topological ring and `D` is an `R`-algebra, finite as an `R`-module,
and if `D` is given the module topology, then `D` is a topological ring.  -/
IsModuleTopology.isTopologicalRing : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : TopologicalSpace R] [IsTopologicalRing R] (D : Type u_2)
  [inst_3 : Ring D] [inst_4 : Algebra R D] [Module.Finite R D] [inst_6 : TopologicalSpace D] [IsModuleTopology R D],
  IsTopologicalRing D
-- Init.Data.Format.Basic
_private.Init.Data.Format.Basic.0.Std.Format.WorkGroup.items : Std.Format.WorkGroup✝ → List Std.Format.WorkItem✝
-- Init.Data.Int.Order
Int.lt_sub_right_iff_add_lt : ∀ {a b c : ℤ}, a < c - b ↔ a + b < c
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- a morphism between the third lines  -/
CategoryTheory.ShortComplex.SnakeInput.Hom.f₃ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {S₁ S₂ : CategoryTheory.ShortComplex.SnakeInput C} → S₁.Hom S₂ → (S₁.L₃ ⟶ S₂.L₃)
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.mem_closure_iff_forall_mem_isFlat : ∀ {α : Type u_2} {M : Matroid α} {e : α} (X : Set α),
  autoParam (X ⊆ M.E) Matroid.mem_closure_iff_forall_mem_isFlat._auto_1 →
    (e ∈ M.closure X ↔ ∀ (F : Set α), M.IsFlat F → X ⊆ F → e ∈ F)
-- Mathlib.LinearAlgebra.Quotient.Defs
Submodule.mkQ_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M)
  (x : M), p.mkQ x = Submodule.Quotient.mk x
-- Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
CochainComplex.mappingConeCompHomotopyEquiv_hom_inv_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃),
  CategoryTheory.CategoryStruct.comp (CochainComplex.mappingConeCompHomotopyEquiv f g).hom
      (CochainComplex.mappingConeCompHomotopyEquiv f g).inv =
    CategoryTheory.CategoryStruct.id (CochainComplex.mappingCone g)
-- Lean.Meta.Instances
Lean.Meta.getInstanceAttrKind? : Lean.Name → Lean.CoreM (Option Lean.AttributeKind)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.insertManyIfNewUnit_list_singleton : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap α Unit cmp} {k : α},
  t.insertManyIfNewUnit [k] = t.insertIfNew k ()
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instHashableSymbolKind.hash : Lean.Lsp.SymbolKind → UInt64
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueD_insertEntry_self : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {k : α} {fallback v : β},
  Std.Internal.List.getValueD k (Std.Internal.List.insertEntry k v l) fallback = v
-- Mathlib.NumberTheory.NumberField.House
_private.Mathlib.NumberTheory.NumberField.House.0.NumberField.house.ξ.eq_1 : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] {β : Type u_3} (x : β × (K →+* ℂ) → ℤ) (l : β),
  NumberField.house.ξ✝ K x l = ∑ r, ↑(x (l, r)) * (NumberField.house.newBasis✝ K) r
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.min?_insert_le_min? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [inst : Std.TransCmp cmp] (h : t.WF) {k km kmi : α},
  t.min? = some km → (t.insert k).min?.get ⋯ = kmi → (cmp kmi km).isLE = true
-- Init.Data.Nat.Lemmas
/-- `m` is not divisible by `n` if it is between `n * k` and `n * (k + 1)` for some `k`.  -/
Nat.not_dvd_of_lt_of_lt_mul_succ : ∀ {n k m : ℕ}, n * k < m → m < n * (k + 1) → ¬n ∣ m
-- Mathlib.CategoryTheory.Sites.Subsheaf
CategoryTheory.Subfunctor.eq_sheafify_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {F : CategoryTheory.Functor Cᵒᵖ (Type w)} (G : CategoryTheory.Subfunctor F),
  CategoryTheory.Presieve.IsSheaf J F →
    (G = CategoryTheory.Subfunctor.sheafify J G ↔ CategoryTheory.Presieve.IsSheaf J G.toFunctor)
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubMulAction.ofFixingSubgroup.append_left : ∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {s : Set α} {n : ℕ} [inst_2 : Finite ↑s]
  (x : Fin n ↪ ↥(SubMulAction.ofFixingSubgroup M s)) (i : Fin s.ncard),
  have Hs := ⋯;
  (SubMulAction.ofFixingSubgroup.append x) (Fin.castAdd n i) = ↑((Classical.choice Hs) i)
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int16.instLawfulUpwardEnumerable : Std.PRange.LawfulUpwardEnumerable Int16
-- Mathlib.Topology.DiscreteSubset
IsOpenMap.isDiscrete_range : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y}
  [DiscreteTopology X], IsOpenMap f → IsDiscrete (Set.range f)
-- Lean.DocString.Parser
Lean.Doc.Parser.instDecidableEqOrderedListType : DecidableEq Lean.Doc.Parser.OrderedListType
-- Aesop.Script.Step
Aesop.Script.LazyStep.BuildInput.tacticBuilder : {α : Type} → Aesop.Script.LazyStep.BuildInput α → α → Aesop.Script.TacticBuilder
-- Mathlib.Order.Types.Arithmetic
/-- The cardinal of an `OrderType` is the cardinality of any type on which a relation
with that order type is defined.  -/
OrderType.card : OrderType.{u_1} → Cardinal.{u_1}
-- Mathlib.Order.Filter.Map
Function.Semiconj.filter_map : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {ga : α → α} {gb : β → β},
  Function.Semiconj f ga gb → Function.Semiconj (Filter.map f) (Filter.map ga) (Filter.map gb)
-- Mathlib.Topology.Covering.Quotient
IsQuotientCoveringMap.subgroup_congr : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] (f : E → X) (G : Type u_3)
  [inst_2 : Group G] [inst_3 : MulAction G E] (S S' : Subgroup G),
  S = S' → (IsQuotientCoveringMap f ↥S ↔ IsQuotientCoveringMap f ↥S')
-- Mathlib.Algebra.Ring.Aut
RingAut.one_apply : ∀ {R : Type u_1} [inst : Mul R] [inst_1 : Add R] (x : R), 1 x = x
-- Mathlib.GroupTheory.DoubleCoset
DoubleCoset.disjoint_out : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} {a b : DoubleCoset.Quotient ↑H ↑K},
  a ≠ b → Disjoint (DoubleCoset.doubleCoset (Quotient.out a) ↑H ↑K) (DoubleCoset.doubleCoset (Quotient.out b) ↑H ↑K)
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
/-- A vector field on a vector space is `C^n` in the manifold sense iff it is `C^n` in the vector
space sense.  -/
contMDiffOn_vectorSpace_iff_contDiffOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V : (x : E) → TangentSpace (modelWithCornersSelf 𝕜 E) x} {s : Set E},
  ContMDiffOn (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E).tangent n (fun x => ⟨x, V x⟩) s ↔ ContDiffOn 𝕜 n V s
-- Init.Meta.Defs
Lean.Syntax.instCoeOutSepArrayArray : {sep : String} → CoeOut (Lean.Syntax.SepArray sep) (Array Lean.Syntax)
-- Mathlib.Topology.ClusterPt
clusterPt_iff_frequently' : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {F : Filter X}, ClusterPt x F ↔ ∀ s ∈ F, ∃ᶠ (y : X) in nhds x, y ∈ s
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
CategoryTheory.Functor.isTerminalConst_from_app : ∀ (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] {X : D} (hX : CategoryTheory.Limits.IsTerminal X)
  (F : CategoryTheory.Functor C D) (Y : C),
  ((CategoryTheory.Functor.isTerminalConst C hX).from F).app Y = hX.from (F.obj Y)
-- Batteries.Tactic.GeneralizeProofs
/-- Runs `MAbs` in `MGen`. Returns the value and the `generalizations`.  -/
Batteries.Tactic.GeneralizeProofs.MGen.runMAbs : {α : Type} →
  Batteries.Tactic.GeneralizeProofs.MAbs α → Batteries.Tactic.GeneralizeProofs.MGen (α × Array (Lean.Expr × Lean.Expr))
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X Y : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C} (α : X ⟶ Y),
  (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon C).map α =
    ((CategoryTheory.Functor.mapMonFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C).map α).app
      (CategoryTheory.Mon.trivial (CategoryTheory.Discrete PUnit.{w + 1}))
-- Mathlib.Analysis.Complex.Trigonometric
Real.cosh_sq' : ∀ (x : ℝ), Real.cosh x ^ 2 = 1 + Real.sinh x ^ 2
-- Mathlib.Order.WellQuasiOrder
instWellQuasiOrderedLEProd : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [WellQuasiOrderedLE α] [inst_2 : Preorder β] [WellQuasiOrderedLE β],
  WellQuasiOrderedLE (α × β)
-- Mathlib.Analysis.Complex.CauchyIntegral
/-- **Cauchy integral formula for the first order derivative**, assuming `f` is continuous on a
closed ball and differentiable on its interior.  -/
DiffContOnCl.deriv_eq_smul_circleIntegral : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {R : ℝ} {f : ℂ → E} {c : ℂ},
  0 < R →
    DiffContOnCl ℂ f (Metric.ball c R) →
      ∮ (z : ℂ) in C(c, R), (1 / (z - c) ^ 2) • f z = (2 * ↑Real.pi * Complex.I) • deriv f c
-- Mathlib.GroupTheory.SchurZassenhaus
/-- Do not use this lemma: It is made obsolete by `exists_right_complement'_of_coprime`  -/
_private.Mathlib.GroupTheory.SchurZassenhaus.0.Subgroup.SchurZassenhausInduction.step1 : ∀ {G : Type u} [inst : Group G] {N : Subgroup G} [N.Normal],
  (Nat.card ↥N).Coprime N.index →
    (∀ (G' : Type u) [inst : Group G'] [Finite G'],
        Nat.card G' < Nat.card G →
          ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H') →
      (∀ (H : Subgroup G), ¬N.IsComplement' H) → ∀ [Finite G] (K : Subgroup G), K ⊔ N = ⊤ → K = ⊤
-- Mathlib.Topology.Algebra.UniformRing
UniformSpace.Completion.mapRingHom_comp : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : UniformSpace α] [inst_2 : IsTopologicalRing α] [inst_3 : IsUniformAddGroup α]
  {β : Type u} [inst_4 : UniformSpace β] [inst_5 : Ring β] [inst_6 : IsUniformAddGroup β] [inst_7 : IsTopologicalRing β]
  {f : α →+* β} {γ : Type u_2} [inst_8 : UniformSpace γ] [inst_9 : Ring γ] [inst_10 : IsUniformAddGroup γ]
  [inst_11 : IsTopologicalRing γ] {g : β →+* γ} (hg : Continuous ⇑g) (hf : Continuous ⇑f),
  (UniformSpace.Completion.mapRingHom g hg).comp (UniformSpace.Completion.mapRingHom f hf) =
    UniformSpace.Completion.mapRingHom (g.comp f) ⋯
-- Lean.Server.FileWorker.ExampleHover
/-- Rewrites examples in docstring Markdown for output as hover Markdown.

In particular, code blocks with the `output` class have line comment markers inserted. Editors do
not typically distinguish between code block classes, so some other visual indication is needed to
separate them. This function is not based on a compliant Markdown parser and may give unpredictable
results when used with invalid Markdown.
 -/
Lean.Server.FileWorker.Hover.rewriteExamples : String → String
-- Mathlib.GroupTheory.FreeGroup.Reduce
/-- If words `w₁ w₂` are such that `w₁` reduces to `w₂`, then `w₂` reduces to the
maximal reduction of `w₁`.  -/
FreeAddGroup.reduce.rev : ∀ {α : Type u_1} {L₁ L₂ : List (α × Bool)} [inst : DecidableEq α],
  FreeAddGroup.Red L₁ L₂ → FreeAddGroup.Red L₂ (FreeAddGroup.reduce L₁)
-- Mathlib.Algebra.Group.Submonoid.Defs
MonoidHom.eqLocusM.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (f g : M →* N),
  f.eqLocusM g = { carrier := {x | f x = g x}, mul_mem' := ⋯, one_mem' := ⋯ }
-- Mathlib.Data.List.Lookmap
List.length_lookmap : ∀ {α : Type u_1} (f : α → Option α) (l : List α), (List.lookmap f l).length = l.length
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.mkCoe : Lean.Expr →
  Lean.Expr →
    optParam (Option Lean.Expr) none →
      optParam (Option String) none →
        optParam (Option (Lean.MVarId → Lean.Expr → Lean.Expr → Lean.MetaM Lean.MessageData)) none →
          optParam (Option (Option Lean.MessageData → Lean.Expr → Lean.Expr → Lean.MetaM Lean.MessageData)) none →
            Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Algebra.Star.Unitary
Unitary.map_injective : ∀ {R : Type u_2} {S : Type u_3} [inst : Monoid R] [inst_1 : StarMul R] [inst_2 : Monoid S] [inst_3 : StarMul S]
  {f : R →⋆* S}, Function.Injective ⇑f → Function.Injective ⇑(Unitary.map f)
-- Mathlib.MeasureTheory.Group.Pointwise
MeasurableSet.const_smul : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α]
  [MeasurableConstSMul G α] {s : Set α}, MeasurableSet s → ∀ (a : G), MeasurableSet (a • s)
-- Mathlib.RingTheory.Artinian.Module
isArtinian_range : ∀ {R : Type u_1} {M : Type u_2} {P : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid P]
  [inst_3 : Module R M] [inst_4 : Module R P] (f : M →ₗ[R] P) [IsArtinian R M], IsArtinian R ↥f.range