mathlib-initiative/mathlib-types huggingface dataset:
-- Aesop.Tree.ExtractProof
_private.Aesop.Tree.ExtractProof.0.Aesop.SafePrefixState.mk : Array Lean.MVarId → Aesop.SafePrefixState✝
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
IsPrimitiveRoot.toInteger.congr_simp : ∀ {K : Type u} [inst : Field K] {ζ ζ_1 : K} (e_ζ : ζ = ζ_1) {k k_1 : ℕ} (e_k : k = k_1) [inst_1 : NeZero k]
  (hζ : IsPrimitiveRoot ζ k), hζ.toInteger = ⋯.toInteger
-- Mathlib.Analysis.SpecificLimits.Basic
/-- If `a ≠ 0`, `(a * x + c)⁻¹` tends to `0` as `x` tends to `∞`.  -/
tendsto_mul_add_inv_atTop_nhds_zero : ∀ (a c : ℝ), a ≠ 0 → Filter.Tendsto (fun x => (a * x + c)⁻¹) Filter.atTop (nhds 0)
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.sub_mem : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (L' : LieSubalgebra R L)
  {x y : L}, x ∈ L' → y ∈ L' → x - y ∈ L'
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalAddSubgroup.ext : ∀ {G : Type u_1} {inst : AddGroup G} {x y : FiniteIndexNormalAddSubgroup G}, x.carrier = y.carrier → x = y
-- Mathlib.Algebra.Group.Commute.Basic
AddCommute.addConj_iff : ∀ {G : Type u_1} [inst : AddGroup G] {a b : G} (h : G), AddCommute (h + a + -h) (h + b + -h) ↔ AddCommute a b
-- Mathlib.Data.Num.Basic
/-- Converts `x : Num` to `-x : ZNum`.  -/
Num.toZNumNeg : Num → ZNum
-- Mathlib.Combinatorics.Graph.Delete
Graph.edgeSet_induce : ∀ {α : Type u_1} {β : Type u_2} (G : Graph α β) (X : Set α),
  (G.induce X).edgeSet = {e | ∃ x y, G.IsLink e x y ∧ x ∈ X ∧ y ∈ X}
-- Mathlib.Analysis.Convex.Basic
Convex.semilinear_image : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : PartialOrder 𝕜] {𝕜' : Type u_5}
  [inst_3 : Semiring 𝕜'] [inst_4 : PartialOrder 𝕜'] {σ : 𝕜 →+* 𝕜'} [RingHomSurjective σ] {F' : Type u_6}
  [inst_6 : AddCommMonoid F'] [inst_7 : Module 𝕜' F'] [inst_8 : Module 𝕜 E] {s : Set E},
  Convex 𝕜 s → (∀ {s t : 𝕜}, σ s ≤ σ t ↔ s ≤ t) → ∀ (f : E →ₛₗ[σ] F'), Convex 𝕜' (⇑f '' s)
-- Mathlib.RingTheory.Ideal.Quotient.Operations
DoubleQuot.quotQuotEquivQuotOfLE_comp_quotQuotMkₐ : ∀ (R : Type u) {A : Type u_1} [inst : CommSemiring R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {I J : Ideal A}
  (h : I ≤ J), (↑(DoubleQuot.quotQuotEquivQuotOfLEₐ R h)).comp (DoubleQuot.quotQuotMkₐ R I J) = Ideal.Quotient.mkₐ R J
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Mon.instMonObjOfIsCommMonObjX.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {M : CategoryTheory.Mon C} [inst_3 : CategoryTheory.IsCommMonObj M.X],
  CategoryTheory.Mon.instMonObjOfIsCommMonObjX =
    { one := { hom := CategoryTheory.MonObj.one, isMonHom_hom := ⋯ },
      mul := { hom := CategoryTheory.MonObj.mul, isMonHom_hom := ⋯ }, one_mul := ⋯, mul_one := ⋯, mul_assoc := ⋯ }
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.NullMeasurable.comp_snd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : β → γ},
  MeasureTheory.NullMeasurable f ν → MeasureTheory.NullMeasurable (fun z => f z.2) (μ.prod ν)
-- Init.Data.Int.Order
Int.ofNat_toNat : ∀ (a : ℤ), ↑a.toNat = max a 0
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue_cons : ∀ {α : Type u} {β : Type v} [inst : BEq α] {l : List ((_ : α) × β)} {k a : α} {v : β}
  {h : Std.Internal.List.containsKey a (⟨k, v⟩ :: l) = true},
  Std.Internal.List.getValue a (⟨k, v⟩ :: l) h = if h' : (k == a) = true then v else Std.Internal.List.getValue a l ⋯
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.DifferentialObject.Hom.comm_assoc : ∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S]
  {X Y : CategoryTheory.DifferentialObject S C} (self : X.Hom Y) {Z : C}
  (h : (CategoryTheory.shiftFunctor C 1).obj Y.obj ⟶ Z),
  CategoryTheory.CategoryStruct.comp X.d
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C 1).map self.f) h) =
    CategoryTheory.CategoryStruct.comp self.f (CategoryTheory.CategoryStruct.comp Y.d h)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey_eq_maxKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {he : t.isEmpty = false}, t.maxKey he = t.maxKey!
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.toFun_eq_coe : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] (f : E →ₛₗ.[σ] F)
  (x : ↥f.domain), f.toFun x = ↑f x
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.State.mk : Array Lean.Meta.Grind.Arith.Linear.Struct →
  Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ) →
    Lean.PHashMap Lean.Meta.Sym.ExprPtr ℕ →
      Lean.PArray (Lean.Expr × ℕ) →
        Lean.PHashSet Lean.Meta.Sym.ExprPtr →
          Array Lean.Meta.Grind.Arith.Linear.NatStruct →
            Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ) →
              Lean.PHashMap Lean.Meta.Sym.ExprPtr ℕ → Lean.Meta.Grind.Arith.Linear.State
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_eq_some_getKey!_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {a : α}, t.contains a = true → t.getKey? a = some (t.getKey! a)
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.proj_symm_apply' : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  (e : Bundle.Pretrivialization F proj) {b : B} {x : F}, b ∈ e.baseSet → proj (↑e.symm (b, x)) = b
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.IsQuasiInverse.congr : ∀ {K : Type u_1} {V₂ : Type u_4} {V₃ : Type u_6} [inst : CommRing K] [inst_1 : AddCommGroup V₂] [inst_2 : Module K V₂]
  [inst_3 : AddCommGroup V₃] [inst_4 : Module K V₃] {u u' : V₃ →ₗ[K] V₂} {v v' : V₂ →ₗ[K] V₃},
  u.IsQuasiInverse v → u' ≈ u → v' ≈ v → u'.IsQuasiInverse v'
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.indepFun_iff_map_prod_eq_prod_map_map' : ∀ {Ω : Type u_1} {β : Type u_6} {β' : Type u_7} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : Ω → β}
  {g : Ω → β'} {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'},
  AEMeasurable f μ →
    AEMeasurable g μ →
      MeasureTheory.SigmaFinite (MeasureTheory.Measure.map f μ) →
        MeasureTheory.SigmaFinite (MeasureTheory.Measure.map g μ) →
          (ProbabilityTheory.IndepFun f g μ ↔
            MeasureTheory.Measure.map (fun ω => (f ω, g ω)) μ =
              (MeasureTheory.Measure.map f μ).prod (MeasureTheory.Measure.map g μ))
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.lift_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → Z ⟶ F.obj x)
  (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (M x) (F.map f) = M y)
  {X Y : CategoryTheory.WithInitial C} (f : X ⟶ Y),
  (CategoryTheory.WithInitial.lift F M hM).map f =
    match X, Y, f with
    | CategoryTheory.WithInitial.of a, CategoryTheory.WithInitial.of a_1, f => F.map (CategoryTheory.WithInitial.down f)
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of a, x => M a
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, x =>
      CategoryTheory.CategoryStruct.id
        (match CategoryTheory.WithInitial.star with
        | CategoryTheory.WithInitial.of x => F.obj x
        | CategoryTheory.WithInitial.star => Z)
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
addRothNumber_Ico : ∀ (a b : ℕ), addRothNumber (Finset.Ico a b) = rothNumberNat (b - a)
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurableSet_stopping_time_le : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
  {τ π : Ω → WithTop ι} [inst_1 : TopologicalSpace ι] [SecondCountableTopology ι] [OrderTopology ι],
  MeasureTheory.IsStoppingTime f τ → ∀ (hπ : MeasureTheory.IsStoppingTime f π), MeasurableSet {ω | τ ω ≤ π ω}
-- Init.Grind.ToInt
Lean.Grind.ToInt.OfNat.mk : ∀ {α : Type u} [inst : (n : ℕ) → OfNat α n] {I : outParam Lean.Grind.IntInterval} [inst_1 : Lean.Grind.ToInt α I],
  (∀ (n : ℕ), ↑(OfNat.ofNat n) = I.wrap ↑n) → Lean.Grind.ToInt.OfNat α I
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.hom_ext₀_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {F G : CategoryTheory.ComposableArrows C 0}
  {φ φ' : F ⟶ G},
  φ = φ' ↔
    CategoryTheory.ComposableArrows.app' φ 0 CategoryTheory.ComposableArrows.homMk₀._proof_1 =
      CategoryTheory.ComposableArrows.app' φ' 0 CategoryTheory.ComposableArrows.homMk₀._proof_1
-- Mathlib.Algebra.BigOperators.Intervals
Finset.prod_range_reflect : ∀ {M : Type u_3} [inst : CommMonoid M] (f : ℕ → M) (n : ℕ),
  ∏ j ∈ Finset.range n, f (n - 1 - j) = ∏ j ∈ Finset.range n, f j
-- Lean.Meta.RecursorInfo
Lean.Meta.RecursorUnivLevelPos.majorType.inj : ∀ {idx idx_1 : ℕ},
  Lean.Meta.RecursorUnivLevelPos.majorType idx = Lean.Meta.RecursorUnivLevelPos.majorType idx_1 → idx = idx_1
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.Karoubi.eqToHom_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P Q : CategoryTheory.Idempotents.Karoubi C} (h : P = Q),
  (CategoryTheory.eqToHom h).f = CategoryTheory.CategoryStruct.comp P.p (CategoryTheory.eqToHom ⋯)
-- Init.Data.Option.Monadic
Option.forIn'_join : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [inst : Monad m] [LawfulMonad m] (b : β)
  (o : Option (Option α)) (f : (a : α) → a ∈ o.join → β → m (ForInStep β)),
  forIn' o.join b f = forIn' o b fun o' ho' b => ForInStep.yield <$> forIn' o' b fun a ha b' => f a ⋯ b'
-- Mathlib.Data.Finsupp.Pointwise
Finsupp.instNonUnitalSemiring : {α : Type u₁} → {β : Type u₂} → [inst : NonUnitalSemiring β] → NonUnitalSemiring (α →₀ β)
-- Mathlib.MeasureTheory.VectorMeasure.WithDensity
MeasureTheory.withDensityᵥ_add' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {f g : α → E},
  MeasureTheory.Integrable f μ →
    MeasureTheory.Integrable g μ → (μ.withDensityᵥ fun x => f x + g x) = μ.withDensityᵥ f + μ.withDensityᵥ g
-- Mathlib.FieldTheory.RatFunc.Basic
/-- `K⟮X⟯` is a commutative monoid.

This is an intermediate step on the way to the full instance `RatFunc.instCommRing`.
 -/
RatFunc.instCommMonoid : (K : Type u) → [inst : CommRing K] → CommMonoid (RatFunc K)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.contains_unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp] {l : List α} {k : α},
  (Std.TreeMap.unitOfList l cmp).contains k = l.contains k
-- Mathlib.CategoryTheory.Shift.Adjunction
CategoryTheory.Adjunction.LeftAdjointCommShift.iso_inv_app_assoc : ∀ {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] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) {A : Type u_3} [inst_2 : AddGroup A] [inst_3 : CategoryTheory.HasShift C A]
  [inst_4 : CategoryTheory.HasShift D A] (a b : A) (h : a + b = 0) [inst_5 : G.CommShift A] (Y : C) {Z : D}
  (h_1 : F.obj ((CategoryTheory.shiftFunctor C a).obj Y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Adjunction.LeftAdjointCommShift.iso adj a).inv.app Y) h_1 =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.shiftFunctor D a).map (F.map ((CategoryTheory.shiftFunctorCompIsoId C a b h).inv.app Y)))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor D a).map
          (F.map ((CategoryTheory.shiftFunctor C b).map (adj.unit.app ((CategoryTheory.shiftFunctor C a).obj Y)))))
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.shiftFunctor D a).map
            (F.map
              ((CategoryTheory.Functor.commShiftIso G b).inv.app (F.obj ((CategoryTheory.shiftFunctor C a).obj Y)))))
          (CategoryTheory.CategoryStruct.comp
            ((CategoryTheory.shiftFunctor D a).map
              (adj.counit.app
                ((CategoryTheory.shiftFunctor D b).obj (F.obj ((CategoryTheory.shiftFunctor C a).obj Y)))))
            (CategoryTheory.CategoryStruct.comp
              ((CategoryTheory.shiftFunctorCompIsoId D b a ⋯).hom.app (F.obj ((CategoryTheory.shiftFunctor C a).obj Y)))
              h_1))))
-- Std.Do.WP.Sound
_private.Std.Do.WP.Sound.0.Std.Do.instWPSoundExceptTExceptPureOfLawfulMonad.match_5.eq_1 : ∀ {ε α : Type u_1} {P : α → Prop}
  (motive :
    (r : Except ε α) →
      (match r with
        | Except.ok a => P a
        | Except.error a => True) →
        Sort u_2)
  (a : α)
  (hp :
    match Except.ok a with
    | Except.ok a => P a
    | Except.error a => True)
  (h_1 :
    (a : α) →
      (hp :
          match Except.ok a with
          | Except.ok a => P a
          | Except.error a => True) →
        motive (Except.ok a) hp)
  (h_2 :
    (e : ε) →
      (x :
          match Except.error e with
          | Except.ok a => P a
          | Except.error a => True) →
        motive (Except.error e) x),
  (match Except.ok a, hp with
    | Except.ok a, hp => h_1 a hp
    | Except.error e, x => h_2 e x) =
    h_1 a hp
-- Mathlib.RingTheory.LocalProperties.Basic
RingHom.OfLocalizationSpanTarget.ofIsLocalization : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.OfLocalizationSpanTarget fun {R S} [CommRing R] [CommRing S] => P) →
    (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P) →
      ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Set S),
        Ideal.span s = ⊤ →
          (∀ (r : ↑s), ∃ T x x_1, ∃ (_ : IsLocalization.Away (↑r) T), P ((algebraMap S T).comp f)) → P f
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.all_eq_false' : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [LawfulBEq α] {p : α → β → Bool},
  (↑m).WF →
    ((↑m).all p = false ↔ ∃ a, ∃ (h : m.contains a = true), p a (Std.DHashMap.Internal.Raw₀.Const.get m a h) = false)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.mk : {G : Type u} →
  [inst : TopologicalSpace G] →
    {H : Type v} →
      [inst_1 : TopologicalSpace H] →
        [inst_2 : Add G] →
          [inst_3 : Add H] →
            (toAddEquiv : G ≃+ H) →
              autoParam (Continuous toAddEquiv.toFun) Homeomorph.continuous_toFun._autoParam →
                autoParam (Continuous toAddEquiv.invFun) Homeomorph.continuous_invFun._autoParam → G ≃ₜ+ H
-- Init.Data.Fin.Lemmas
Fin.ne_of_lt : ∀ {n : ℕ} {a b : Fin n}, a < b → a ≠ b
-- Mathlib.Dynamics.Minimal
denseRange_vadd : ∀ (M : Type u_1) {α : Type u_3} [inst : AddMonoid M] [inst_1 : TopologicalSpace α] [inst_2 : AddAction M α]
  [AddAction.IsMinimal M α] (x : α), DenseRange fun c => c +ᵥ x
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.pow_sub_dvd_iterate_derivative_pow : ∀ {R : Type u} [inst : CommSemiring R] (p : Polynomial R) (n m : ℕ), p ^ (n - m) ∣ (⇑Polynomial.derivative)^[m] (p ^ n)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.size_filter_eq_size_iff : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α] {f : (a : α) → β a → Bool},
  (↑m).WF →
    ((↑(Std.DHashMap.Internal.Raw₀.filter f m)).size = (↑m).size ↔
      ∀ (a : α) (h : m.contains a = true), f a (m.get a h) = true)
-- Mathlib.Topology.UniformSpace.LocallyUniformConvergence
TendstoLocallyUniformlyOn.congr_inseparable : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {F : ι → α → β}
  {f : α → β} {s : Set α} {p : Filter ι} {G : ι → α → β},
  TendstoLocallyUniformlyOn F f p s →
    (∀ᶠ (n : ι) in p, ∀ x ∈ s, Inseparable (F n x) (G n x)) → TendstoLocallyUniformlyOn G f p s
-- Mathlib.GroupTheory.Index
/-- Relative version of `Subgroup.index_dvd_two_iff`.  -/
Subgroup.relIndex_dvd_two_iff : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, H.relIndex K ∣ 2 ↔ ∃ a ∈ K, ∀ b ∈ K, b * a ∈ H ∨ b ∈ H
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Generators.cotangentRestrict.eq_1 : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type w}
  (P : Algebra.Generators R S ι) {σ : Type u_1} {u : σ → ι} (hu : Function.Injective u),
  P.cotangentRestrict hu = Finsupp.lcomapDomain u hu ∘ₗ ↑P.cotangentSpaceBasis.repr ∘ₗ P.toExtension.cotangentComplex
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
/-- The objects over `X i` for all `i`  -/
CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.obj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F :
        CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
          (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)} →
      {ι : Type t} →
        {S : C} →
          {X : ι → C} →
            {f : (i : ι) → X i ⟶ S} → F.DescentDataAsCoalgebra f → (i : ι) → ↑(F.obj { as := Opposite.op (X i) }).obj
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHom.copy_eq : ∀ {M : Type u_4} {N : Type u_5} {x : AddZero M} {x_1 : AddZero N} (f : M →+ N) (f' : M → N) (h : f' = ⇑f),
  f.copy f' h = f
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
/-- In the specific case of continuous alternating maps on spaces indexed by `Fin (n+1)`, where one
can build an element of `Π(i : Fin (n+1)), M i` using `cons`, one can express directly the
multiplicativity of an alternating map along the first variable.  -/
ContinuousAlternatingMap.vecCons_smul : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N] [inst_6 : TopologicalSpace N] {n : ℕ}
  (f : M [⋀^Fin (n + 1)]→L[R] N) (m : Fin n → M) (c : R) (x : M),
  f (Matrix.vecCons (c • x) m) = c • f (Matrix.vecCons x m)
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
contMDiff_of_contMDiffOn_union_of_isOpen : ∀ {𝕜 : 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] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_7 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7}
  [inst_8 : TopologicalSpace M'] [inst_9 : ChartedSpace H M] [inst_10 : ChartedSpace H' M'] {f : M → M'}
  {n : WithTop ℕ∞} {s t : Set M},
  ContMDiffOn I I' n f s → ContMDiffOn I I' n f t → s ∪ t = Set.univ → IsOpen s → IsOpen t → ContMDiff I I' n f
-- Init.Data.AC
Lean.Data.AC.Context.evalList_insert : ∀ {α : Sort u_1} (ctx : Lean.Data.AC.Context α),
  Std.Commutative ctx.op →
    ∀ (x : ℕ) (xs : List ℕ),
      Lean.Data.AC.evalList α ctx (Lean.Data.AC.insert x xs) = Lean.Data.AC.evalList α ctx (x :: xs)
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.IsPosSemidef.smul : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Preorder R] [PosMulMono R] {B : LinearMap.BilinForm R M} {c : R},
  B.IsPosSemidef → 0 ≤ c → (c • B).IsPosSemidef
-- Mathlib.RingTheory.Localization.Integer
/-- Each element `a : S` has an `M`-multiple which is an integer.

This version multiplies `a` on the left, matching the argument order in the `SMul` instance.
 -/
IsLocalization.exists_integer_multiple : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] (a : S), ∃ b, IsLocalization.IsInteger R (↑b • a)
-- Lean.Meta.Tactic.Simp.Arith.Nat.Basic
Lean.Meta.Simp.Arith.Nat.instReprExpr_lean : Repr Nat.Internal.Linear.Expr
-- Mathlib.NumberTheory.LSeries.ZetaZeros
tendsto_riemannZeta_cofinite_cocompact : Filter.Tendsto Subtype.val Filter.cofinite (Filter.cocompact ℂ)
-- Mathlib.CategoryTheory.CatCommSq
CategoryTheory.CatCommSq.hInv_hInv : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄] (T : C₁ ≌ C₂) (L : CategoryTheory.Functor C₁ C₃)
  (R : CategoryTheory.Functor C₂ C₄) (B : C₃ ≌ C₄) (h : CategoryTheory.CatCommSq T.functor L R B.functor),
  CategoryTheory.CatCommSq.hInv T.symm R L B.symm (CategoryTheory.CatCommSq.hInv T L R B h) = h
-- Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
CategoryTheory.MorphismProperty.IsInvertedBy.iff_map_le_isomorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (W : CategoryTheory.MorphismProperty C) (F : CategoryTheory.Functor C D),
  W.IsInvertedBy F ↔ W.map F ≤ CategoryTheory.MorphismProperty.isomorphisms D
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.isCompact_Icc : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι), IsCompact (BoxIntegral.Box.Icc I)
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.mulRight_apply : ∀ {G : Type v} [inst : Group G] [inst_1 : PseudoEMetricSpace G] [inst_2 : IsIsometricSMul Gᵐᵒᵖ G] (c x : G),
  (IsometryEquiv.mulRight c) x = x * c
-- Lean.Meta.LazyDiscrTree
/-- `findMatchesExt` searches for entries in a lazily initialized discriminator tree.

It provides some additional capabilities beyond `findMatches` to adjust results
based on priority and cache module declarations

* `modulesTreeRef` points to the discriminator tree for local environment.
  Used for caching and created by `createLocalTree`.
* `ref` is a process-global `IO.Ref` for caching the import lazy discriminator tree.
* `addEntry` is the function for creating discriminator tree entries from constants.
* `droppedKeys` contains keys we do not want to consider when searching for matches.
  It is used for dropping very general keys.
* `constantsPerTask` stores number of constants in imported modules used to
  decide when to create new task.
* `adjustResult` takes the priority and value to produce a final result.
* `ty` is the expression type.
 -/
Lean.Meta.LazyDiscrTree.findMatchesExt : {α β : Type} →
  Lean.Meta.LazyDiscrTree.ModuleDiscrTreeRef α →
    IO.Ref (Option (Lean.Meta.LazyDiscrTree α)) →
      (Lean.Name → Lean.AsyncConstantInfo → Lean.MetaM (Array (Lean.Meta.LazyDiscrTree.InitEntry α))) →
        optParam (List (List Lean.Meta.LazyDiscrTree.Key)) [] →
          optParam ℕ 1000 →
            optParam (Option (IO.Ref (Option (Array α)))) none → (ℕ → α → β) → Lean.Expr → Lean.MetaM (Array β)
-- Init.Data.List.Basic
List.beq_nil_nil : ∀ {α : Type u} [inst : BEq α], [].beq [] = true
-- Mathlib.CategoryTheory.Sites.Sheafification
CategoryTheory.sheafification_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type u_1)
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  (P : CategoryTheory.Functor Cᵒᵖ D), (CategoryTheory.sheafification J D).obj P = CategoryTheory.sheafify J P
-- Mathlib.Algebra.Ring.Subsemiring.Pointwise
Subsemiring.smul_mem_pointwise_smul : ∀ {M : Type u_1} {R : Type u_2} [inst : Monoid M] [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R] (m : M) (r : R)
  (S : Subsemiring R), r ∈ S → m • r ∈ m • S
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.Icc_subset_uIcc' : ∀ {α : Type u_1} [inst : Lattice α] {a b : α}, Set.Icc b a ⊆ Set.uIcc a b
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Complex.tan_ne_zero_iff : ∀ {θ : ℂ}, Complex.tan θ ≠ 0 ↔ ∀ (k : ℤ), ↑k * ↑Real.pi / 2 ≠ θ