mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.instIsAddRightInvariantForallVolumeOfMeasurableAddOfSigmaFinite : ∀ {ι : Type u_1} [inst : Fintype ι] {G : ι → Type u_4} [inst_1 : (i : ι) → AddGroup (G i)]
  [inst_2 : (i : ι) → MeasureTheory.MeasureSpace (G i)] [∀ (i : ι), MeasurableAdd (G i)]
  [∀ (i : ι), MeasureTheory.SigmaFinite MeasureTheory.volume] [∀ (i : ι), MeasureTheory.volume.IsAddRightInvariant],
  MeasureTheory.volume.IsAddRightInvariant
-- Mathlib.RingTheory.Etale.QuasiFinite
Ideal.comap_fiberIsoOfBijectiveResidueField_apply : ∀ {R : Type u_1} {R' : Type u_2} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing R'] [inst_2 : CommRing S]
  [inst_3 : Algebra R R'] [inst_4 : Algebra R S] {p : Ideal R} {q : Ideal R'} [inst_5 : p.IsPrime] [inst_6 : q.IsPrime]
  [inst_7 : q.LiesOver p] (H : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p q (Algebra.ofId R R') ⋯))
  (Q : ↑(q.primesOver (TensorProduct R R' S))),
  ↑((Ideal.fiberIsoOfBijectiveResidueField H) Q) = Ideal.comap Algebra.TensorProduct.includeRight ↑Q
-- Batteries.Data.MLList.Basic
/-- Take the first `n` elements.  -/
MLList.take : {m : Type u_1 → Type u_1} → {α : Type u_1} → [Monad m] → MLList m α → ℕ → MLList m α
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.comp.eq_1 : ∀ {M : Type u_2} {N : Type u_3} {P : Type u_4} {φ : M → N} {ψ : N → P} {χ : M → P} {X : Type u_5} [inst : VAdd M X]
  {Y : Type u_6} [inst_1 : VAdd N Y] {Z : Type u_7} [inst_2 : VAdd P Z] (g : Y →ₑ[ψ] Z) (f : X →ₑ[φ] Y)
  [κ : CompTriple φ ψ χ], g.comp f = { toFun := fun x => g (f x), map_vadd' := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.whiskerLeft_δ_μ_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (X Y : C) (T : D) {Z : D}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj T (F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft T (CategoryTheory.Functor.OplaxMonoidal.δ F X Y))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft T (CategoryTheory.Functor.LaxMonoidal.μ F X Y)) h) =
    h
-- Init.MetaTypes
/-- When simp discharges side conditions for conditional lemmas, it can recursively apply simplification.
The `maxDischargeDepth` (default: 2) is the maximum recursion depth when recursively applying simplification to side conditions.
 -/
Lean.Meta.Simp.Config.maxDischargeDepth : Lean.Meta.Simp.Config → ℕ
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.map₂IdIso.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : CategoryTheory.Functor C D} (α : (CategoryTheory.Functor.id C).comp S ⟶ S.comp (CategoryTheory.Functor.id D))
  (T : D) (β : (CategoryTheory.Functor.id D).obj T ⟶ T)
  (hα : α = CategoryTheory.CategoryStruct.comp S.leftUnitor.hom S.rightUnitor.inv)
  (hβ : β = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id D).obj T)),
  CategoryTheory.CostructuredArrow.map₂IdIso α T β hα hβ = CategoryTheory.CostructuredArrow.map₂IdIso α T β hα hβ
-- Lean.Elab.PreDefinition.Structural.RecArgInfo
Lean.Elab.Structural.RecArgInfo.mk.sizeOf_spec : ∀ (fnName : Lean.Name) (fixedParamPerm : Lean.Elab.FixedParamPerm) (recArgPos : ℕ) (indicesPos : Array ℕ)
  (indGroupInst : Lean.Elab.Structural.IndGroupInst) (indIdx : ℕ),
  sizeOf
      { fnName := fnName, fixedParamPerm := fixedParamPerm, recArgPos := recArgPos, indicesPos := indicesPos,
        indGroupInst := indGroupInst, indIdx := indIdx } =
    1 + sizeOf fnName + sizeOf fixedParamPerm + sizeOf recArgPos + sizeOf indicesPos + sizeOf indGroupInst +
      sizeOf indIdx
-- Mathlib.CategoryTheory.Functor.ReflectsIso.Limits
/-- If `Fᵢ : C ⥤ Dᵢ` is a conservative family of functors which also
preserve the (existing) colimit of a functor `G : J ⥤ C`, then a cocone
for `G` is a colimit if it is so after applying the functors `Fᵢ`
(see also `reflectsColimit_of_reflectsIsomorphisms` in the file
`Mathlib/CategoryTheory/Limits/Preserves/Basic.lean` for the corresponding
result for a single functor)  -/
CategoryTheory.JointlyReflectIsomorphisms.jointlyReflectsColimit : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_5, u_1} C] →
    {I : Type u_2} →
      {D : I → Type u_3} →
        [inst_1 : (i : I) → CategoryTheory.Category.{u_6, u_3} (D i)] →
          {F : (i : I) → CategoryTheory.Functor C (D i)} →
            CategoryTheory.JointlyReflectIsomorphisms F →
              {J : Type u_4} →
                [inst_2 : CategoryTheory.Category.{v_1, u_4} J] →
                  {G : CategoryTheory.Functor J C} →
                    {c : CategoryTheory.Limits.Cocone G} →
                      ((i : I) → CategoryTheory.Limits.IsColimit ((F i).mapCocone c)) →
                        [CategoryTheory.Limits.HasColimit G] →
                          [∀ (i : I), CategoryTheory.Limits.PreservesColimit G (F i)] →
                            CategoryTheory.Limits.IsColimit c
-- Mathlib.MeasureTheory.PiSystem
MeasurableSpace.isPiSystem_measurableSet : ∀ {α : Type u_3} [inst : MeasurableSpace α], IsPiSystem {s | MeasurableSet s}
-- Lean.Meta.Match.Match
Lean.Meta.Match.MkMatcherInput.mk : Lean.Name →
  Lean.Expr →
    Array Lean.Meta.Match.DiscrInfo →
      List Lean.Meta.Match.AltLHS → Option Lean.Meta.Match.Overlaps → Lean.Meta.Match.MkMatcherInput
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.not_matchesAt_endPos : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] {s : String.Slice},
  ¬String.Slice.Pattern.Model.MatchesAt pat s.endPos
-- Mathlib.Analysis.Normed.Operator.Basic
ContinuousLinearMap.homothety_norm : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] [NontrivialTopology E]
  (f : E →SL[σ₁₂] F) {a : ℝ}, (∀ (x : E), ‖f x‖ = a * ‖x‖) → ‖f‖ = a
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.MutualClosure.mkClosureFor : Array Lean.FVarId → Array Lean.LocalDecl → Lean.Elab.TermElabM Lean.Elab.Term.MutualClosure.ClosureState
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Walk.IsPath.neighborSet_toSubgraph_internal : ∀ {V : Type u} {G : SimpleGraph V} {v u : V} {i : ℕ} {p : G.Walk u v},
  p.IsPath → i ≠ 0 → i < p.length → p.toSubgraph.neighborSet (p.getVert i) = {p.getVert (i - 1), p.getVert (i + 1)}
-- Init.Data.Int.Order
Int.natAbs_zero : Int.natAbs 0 = 0
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.mk.injEq : ∀ {R : Type u} {M : Type v} {N : Type w} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (toFun : M → N)
  (toFun_smul : ∀ (a : R) (x : M), toFun (a • x) = (a * a) • toFun x)
  (exists_companion' : ∃ B, ∀ (x y : M), toFun (x + y) = toFun x + toFun y + (B x) y) (toFun_1 : M → N)
  (toFun_smul_1 : ∀ (a : R) (x : M), toFun_1 (a • x) = (a * a) • toFun_1 x)
  (exists_companion'_1 : ∃ B, ∀ (x y : M), toFun_1 (x + y) = toFun_1 x + toFun_1 y + (B x) y),
  ({ toFun := toFun, toFun_smul := toFun_smul, exists_companion' := exists_companion' } =
      { toFun := toFun_1, toFun_smul := toFun_smul_1, exists_companion' := exists_companion'_1 }) =
    (toFun = toFun_1)
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_support : ∀ {X : Type u_1} {M : Type u_5} [inst : NormedAddCommGroup M] [inst_1 : NormedSpace ℝ M] {mX : MeasurableSpace X}
  {ν : MeasureTheory.Measure X} {F : X → M}, ∫ (x : X) in Function.support F, F x ∂ν = ∫ (x : X), F x ∂ν
-- Mathlib.RingTheory.SimpleModule.Basic
IsSimpleModule.congr : ∀ {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_5}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (e : M ≃ₗ[R] N) [IsSimpleModule R N], IsSimpleModule R M
-- Mathlib.CategoryTheory.Localization.Construction
CategoryTheory.Localization.Construction.objEquiv_symm_apply : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] (W : CategoryTheory.MorphismProperty C)
  (X : W.Localization), (CategoryTheory.Localization.Construction.objEquiv W).symm X = X.as.obj
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.contains_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α (fun x => Unit) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List α} {k : α},
  (Std.ExtDTreeMap.Const.insertManyIfNewUnit t l).contains k = (t.contains k || l.contains k)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getD_alter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k k' : α} {fallback : β k'} {f : Option (β k) → Option (β k)},
  (t.alter k f).getD k' fallback =
    if heq : cmp k k' = Ordering.eq then (Option.map (cast ⋯) (f (t.get? k))).getD fallback else t.getD k' fallback
-- Lean.Compiler.IR.Basic
Lean.IR.Decl.params : Lean.IR.Decl → Array Lean.IR.Param
-- Init.Data.List.Lemmas
List.get_eq_getElem : ∀ {α : Type u_1} {l : List α} {i : Fin l.length}, l.get i = l[↑i]
-- Mathlib.Analysis.Calculus.Deriv.Linear
LinearMap.hasStrictDerivAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {x : 𝕜} (e : 𝕜 →ₗ[𝕜] F), HasStrictDerivAt (⇑e) (e 1) x
-- Mathlib.Order.UpperLower.Prod
UpperSet.prod_le_prod_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {s₁ s₂ : UpperSet α} {t₁ t₂ : UpperSet β},
  s₁ ×ˢ t₁ ≤ s₂ ×ˢ t₂ ↔ s₁ ≤ s₂ ∧ t₁ ≤ t₂ ∨ s₂ = ⊤ ∨ t₂ = ⊤
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Subsemiring.op_inf : ∀ {R : Type u_2} [inst : NonAssocSemiring R] (S₁ S₂ : Subsemiring R), (S₁ ⊓ S₂).op = S₁.op ⊓ S₂.op
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toArray_rco_eq_some : ∀ {m n i : ℕ}, i < n - m → (m...n).toArray[i]? = some (m + i)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.map_mono : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B] [inst_5 : Module R B] [inst_6 : Star B]
  [inst_7 : FunLike F A B] [inst_8 : NonUnitalAlgHomClass F R A B] [inst_9 : StarHomClass F A B]
  {S₁ S₂ : NonUnitalStarSubalgebra R A} {f : F},
  S₁ ≤ S₂ → NonUnitalStarSubalgebra.map f S₁ ≤ NonUnitalStarSubalgebra.map f S₂
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
/-- Auxiliary definition for `InjectiveResolution.of`.  -/
CategoryTheory.InjectiveResolution.ofCocomplex : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] → [CategoryTheory.EnoughInjectives C] → C → CochainComplex C ℕ
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.prod_rightr : ∀ {α : Type u_1} {E : Type u_3} {E' : Type u_6} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup E']
  [inst_2 : SeminormedAddCommGroup F'] {f : α → E} (f' : α → E') {g' : α → F'} {l : Filter α},
  f =O[l] g' → f =O[l] fun x => (f' x, g' x)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
one_lt_of_lt_mul_right : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : LT α] [MulLeftReflectLT α] {a b : α}, a < a * b → 1 < b
-- Mathlib.GroupTheory.OrderOfElement
AddMonoid.addOrderOf_eq_one_iff : ∀ {G : Type u_1} [inst : AddMonoid G] {x : G}, addOrderOf x = 1 ↔ x = 0
-- Mathlib.Data.Finsupp.Single
Finsupp.unique_single : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] [inst_1 : Unique α] (x : α →₀ M), x = fun₀ | default => x default
-- Mathlib.Order.Filter.Pointwise
Filter.pure_add : ∀ {α : Type u_2} [inst : Add α] {g : Filter α} {a : α}, pure a + g = Filter.map (fun x => a + x) g
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPullback.isoIsPullback_hom_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : C} (X Y : C) {Z : C} {fst : P ⟶ X} {snd : P ⟶ Y}
  {f : X ⟶ Z} {g : Y ⟶ Z} {P' : C} {fst' : P' ⟶ X} {snd' : P' ⟶ Y} (h : CategoryTheory.IsPullback fst snd f g)
  (h' : CategoryTheory.IsPullback fst' snd' f g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.IsPullback.isoIsPullback X Y h h').hom snd' = snd
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
smoothSheafCommRing.ι_forgetStalk_hom_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {EM : Type u_2} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_3} [inst_3 : TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM)
  {E : Type u_4} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace 𝕜 E] {H : Type u_5} [inst_6 : TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H) (M : Type u) [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace HM M] (R : Type u)
  [inst_9 : TopologicalSpace R] [inst_10 : ChartedSpace H R] [inst_11 : CommRing R] [inst_12 : ContMDiffRing I (↑⊤) R]
  (x : ↑(TopCat.of M)) (U : (TopologicalSpace.OpenNhds x)ᵒᵖ)
  (x_1 :
    ↑((smoothSheafCommRing IM I M R).presheaf.obj
        (Opposite.op ((TopologicalSpace.OpenNhds.inclusion x).obj (Opposite.unop U))))),
  (CategoryTheory.ConcreteCategory.hom (smoothSheafCommRing.forgetStalk IM I M R x).hom)
      ((CommRingCat.Hom.hom
          (CategoryTheory.Limits.colimit.ι
            ((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheafCommRing IM I M R).presheaf) U))
        x_1) =
    (CategoryTheory.ConcreteCategory.hom
        (CategoryTheory.Limits.colimit.ι
          ((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheaf IM I M R).presheaf) U))
      x_1
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
MulAlgebraNorm.instFunLikeReal : {R : outParam (Type u_1)} →
  {S : outParam (Type u_2)} →
    [inst : SeminormedCommRing R] → [inst_1 : Ring S] → [inst_2 : Algebra R S] → FunLike (MulAlgebraNorm R S) S ℝ
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- Orbits of an element form a partition  -/
AddAction.IsPartition.of_orbits : ∀ {G : Type u_1} [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X],
  Setoid.IsPartition (Set.range fun a => AddAction.orbit G a)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.getTarget? : Lean.Expr → Lean.Meta.Grind.GoalM (Option Lean.Expr)
-- Mathlib.NumberTheory.WellApproximable
_private.Mathlib.NumberTheory.WellApproximable.0.AddCircle.«term_∤_» : Lean.TrailingParserDescr
-- Mathlib.Tactic.RenameBVar
/-- Renames a bound variable in the target.  -/
Mathlib.Tactic.renameBVarTarget : Lean.MVarId → Lean.Name → Lean.Name → Lean.MetaM Unit
-- Aesop.Rule.Name
Aesop.RuleName.instOrd : Ord Aesop.RuleName
-- Lean.Meta.Sym.Simp.SimpM
/-- Maximum depth of reentrant simplifier calls through dischargers.
Prevents infinite loops when conditional rewrite rules trigger recursive discharge attempts.
 -/
Lean.Meta.Sym.Simp.Config.maxDischargeDepth : Lean.Meta.Sym.Simp.Config → ℕ
-- Mathlib.LinearAlgebra.RootSystem.Chain
RootPairing.chainTopCoeff_eq_sSup : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : CharZero R] [inst_3 : IsDomain R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsCrystallographic] {i j : ι},
  LinearIndependent R ![P.root i, P.root j] →
    RootPairing.chainTopCoeff i j = sSup {k | P.root j + k • P.root i ∈ Set.range ⇑P.root}
-- Mathlib.Topology.MetricSpace.Completion
/-- Metric space structure on the completion of a `PseudoMetric` space.  -/
UniformSpace.Completion.instMetricSpace : {α : Type u} → [inst : PseudoMetricSpace α] → MetricSpace (UniformSpace.Completion α)
-- Mathlib.Algebra.Order.Archimedean.Basic
existsUnique_sub_zsmul_mem_Ico : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] {a : G},
  0 < a → ∀ (b c : G), ∃! m, b - m • a ∈ Set.Ico c (c + a)
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- An orbit is a fixed block.  -/
AddAction.IsFixedBlock.orbit : ∀ {G : Type u_1} [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] (a : X),
  AddAction.IsFixedBlock G (AddAction.orbit G a)
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.TransvectionStruct.c : {n : Type u_1} → {R : Type u₂} → Matrix.TransvectionStruct n R → R
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Expr.neg.injEq : ∀ (a a_1 : Lean.Grind.Linarith.Expr), (a.neg = a_1.neg) = (a = a_1)
-- Mathlib.CategoryTheory.Sites.Sieves
/-- When `hg : Sieve.ofArrows Y f g`, this is a morphism `h : W ⟶ Y (i hg)` such
that `h ≫ f (i hg) = g`.  -/
CategoryTheory.Sieve.ofArrows.h : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {I : Type u_1} →
      {X : C} →
        {Y : I → C} →
          {f : (i : I) → Y i ⟶ X} →
            {W : C} →
              {g : W ⟶ X} →
                (hg : (CategoryTheory.Sieve.ofArrows Y f).arrows g) → W ⟶ Y (CategoryTheory.Sieve.ofArrows.i hg)
-- Mathlib.Analysis.RCLike.TangentCone
/-- In a real or complex vector space, a convex set with nonempty interior is a set of unique
differentiability.  -/
uniqueDiffOn_convex_of_isRCLikeNormedField : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [h𝕜 : IsRCLikeNormedField 𝕜] {E : Type u_2}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedSpace ℝ E] {s : Set E},
  Convex ℝ s → (interior s).Nonempty → UniqueDiffOn 𝕜 s
-- Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
/-- If `f (g x) = x` for `x` in a neighborhood of `a` within `s`,
`g` maps a neighborhood of `a` within `s` to a neighborhood of `g a` within `t`,
and `f` has an invertible derivative `f'` at `g a` within `t`,
then `g` has the derivative `f'⁻¹` at `a` within `s`.

This is one of the easy parts of the inverse function theorem: it assumes that we already have an
inverse function.  -/
HasFDerivWithinAt.of_local_left_inverse : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {g : E → F} {f : F → E}
  {f' : F ≃L[𝕜] E} {a : E} {s : Set E} {t : Set F},
  Filter.Tendsto g (nhdsWithin a s) (nhdsWithin (g a) t) →
    HasFDerivWithinAt f (↑f') t (g a) →
      a ∈ s → (∀ᶠ (x : E) in nhdsWithin a s, f (g x) = x) → HasFDerivWithinAt g (↑f'.symm) s a
-- Mathlib.Analysis.Normed.Module.FiniteDimension
AffineEquiv.coe_toHomeomorphOfFiniteDimensional : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type w} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : CompleteSpace 𝕜] {PE : Type u_1} {PF : Type u_2} [inst_6 : MetricSpace PE] [inst_7 : NormedAddTorsor E PE]
  [inst_8 : MetricSpace PF] [inst_9 : NormedAddTorsor F PF] [inst_10 : FiniteDimensional 𝕜 E] (f : PE ≃ᵃ[𝕜] PF),
  ⇑f.toHomeomorphOfFiniteDimensional = ⇑f
-- Mathlib.GroupTheory.Sylow
/-- **Frattini's Argument**: If `N` is a normal subgroup of `G`, and if `P` is a Sylow `p`-subgroup
of `N`, then `N_G(P) ⊔ N = G`.  -/
Sylow.normalizer_sup_eq_top' : ∀ {G : Type u_1} [inst : Group G] {p : ℕ} [Fact (Nat.Prime p)] {N : Subgroup G} [N.Normal] [Finite (Sylow p ↥N)]
  (P : Sylow p G), ↑P ≤ N → Subgroup.normalizer ↑P ⊔ N = ⊤
-- Lean.Parser.Basic
Lean.Parser.OrElseOnAntiquotBehavior.takeLongest : Lean.Parser.OrElseOnAntiquotBehavior
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.instAlgebra : {S : Type u_1} →
  {R : Type u_3} →
    {c₁ c₂ c₃ : R} →
      [inst : CommRing R] → [inst_1 : CommSemiring S] → [Algebra S R] → Algebra S (QuaternionAlgebra R c₁ c₂ c₃)
-- Mathlib.Data.Quot
/-- Descends a function `f : α → β → γ` to quotients of `α` and `β`.  -/
Quot.lift₂ : {α : Sort u_1} →
  {β : Sort u_2} →
    {γ : Sort u_4} →
      {r : α → α → Prop} →
        {s : β → β → Prop} →
          (f : α → β → γ) →
            (∀ (a : α) (b₁ b₂ : β), s b₁ b₂ → f a b₁ = f a b₂) →
              (∀ (a₁ a₂ : α) (b : β), r a₁ a₂ → f a₁ b = f a₂ b) → Quot r → Quot s → γ
-- Mathlib.Order.Concept
upperPolar_iUnion : ∀ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (f : ι → Set α),
  upperPolar r (⋃ i, f i) = ⋂ i, upperPolar r (f i)
-- Mathlib.Algebra.Algebra.Operations
Submodule.top_mul_eq_top_of_mul_eq_one : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] {N P : Submodule R A},
  N * P = 1 → ⊤ * P = ⊤
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
Bundle.contMDiff_zeroSection : ∀ {n : WithTop ℕ∞} (𝕜 : Type u_1) {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  [inst_8 : TopologicalSpace B] [inst_9 : ChartedSpace HB B] [inst_10 : FiberBundle F E]
  [inst_11 : (x : B) → AddCommMonoid (E x)] [inst_12 : (x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E],
  ContMDiff IB (IB.prod (modelWithCornersSelf 𝕜 F)) n (Bundle.zeroSection F E)
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.smulCommClass_right : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {α : Type u_1}
  {β : Type u_2} [inst_3 : SMul α β] [inst_4 : SMul A β] [SMulCommClass α A β] (S : Subalgebra R A),
  SMulCommClass α (↥S) β
-- Mathlib.Combinatorics.Additive.CovBySMul
CovByVAdd.subset_left : ∀ {M : Type u_1} {X : Type u_3} [inst : AddMonoid M] [inst_1 : AddAction M X] {K : ℝ} {A₁ A₂ B : Set X},
  A₁ ⊆ A₂ → CovByVAdd M K A₂ B → CovByVAdd M K A₁ B
-- Mathlib.GroupTheory.GroupAction.Hom
/-- Any type satisfying `MulSemiringActionHomClass` can be cast into `MulSemiringActionHom` via
`MulSemiringActionHomClass.toMulSemiringActionHom`.  -/
MulSemiringActionHom.instCoeTCOfMulSemiringActionSemiHomClassCoeMonoidHom : {M : Type u_1} →
  [inst : Monoid M] →
    {N : Type u_2} →
      [inst_1 : Monoid N] →
        {φ : M →* N} →
          {R : Type u_10} →
            [inst_2 : Semiring R] →
              [inst_3 : MulSemiringAction M R] →
                {S : Type u_12} →
                  [inst_4 : Semiring S] →
                    [inst_5 : MulSemiringAction N S] →
                      {F : Type u_15} →
                        [inst_6 : FunLike F R S] → [MulSemiringActionSemiHomClass F (⇑φ) R S] → CoeTC F (R →ₑ+*[φ] S)
-- Mathlib.Data.FunLike.Equiv
EquivLike.coe_apply : ∀ {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} [inst : EquivLike E α β] {e : E} {a : α}, EquivLike.coe e a = e a
-- Batteries.Data.AssocList
Batteries.AssocList.findEntryP?.eq_def : ∀ {α : Type u_1} {β : Type u_2} (p : α → β → Bool) (x : Batteries.AssocList α β),
  Batteries.AssocList.findEntryP? p x =
    match x with
    | Batteries.AssocList.nil => none
    | Batteries.AssocList.cons k v es => bif p k v then some (k, v) else Batteries.AssocList.findEntryP? p es
-- Mathlib.Logic.Relation
Relation.EqvGen.is_equivalence : ∀ {α : Type u_1} (r : α → α → Prop), Equivalence (Relation.EqvGen r)
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
MDifferentiableAt.clm_comp : ∀ {𝕜 : 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] {F₁ : Type u_14} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_15} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {F₃ : Type u_16} [inst_10 : NormedAddCommGroup F₃] [inst_11 : NormedSpace 𝕜 F₃] {g : M → F₁ →L[𝕜] F₃}
  {f : M → F₂ →L[𝕜] F₁} {x : M}, MDiffAt g x → MDiffAt f x → (MDiffAt fun x => g x ∘SL f x) x