mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Matroid.Closure
/-- **Alias** of `Matroid.indep_iff_forall_notMem_closure_sdiff`. -/
Matroid.indep_iff_forall_notMem_closure_diff : ∀ {α : Type u_2} {M : Matroid α} {I : Set α},
  autoParam (I ⊆ M.E) Matroid.indep_iff_forall_notMem_closure_sdiff._auto_1 →
    (M.Indep I ↔ ∀ ⦃e : α⦄, e ∈ I → e ∉ M.closure (I \ {e}))
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.List.popWhile_toArray_aux : ∀ {α : Type u_1} (p : α → Bool) (l : List α), Array.popWhile p l.reverse.toArray = (List.dropWhile p l).reverse.toArray
-- Mathlib.Order.Bounded
Set.bounded_ge_Ico : ∀ {α : Type u_1} [inst : Preorder α] (a b : α), Set.Bounded (fun x1 x2 => x1 ≥ x2) (Set.Ico a b)
-- Mathlib.Analysis.Meromorphic.Basic
/-- If `f` is meromorphic at `x`, then `f - g` is meromorphic at `x` if and only if `g` is meromorphic
at `x`.
 -/
MeromorphicAt.meromorphicAt_sub_iff_meromorphicAt₁ : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : 𝕜} {f g : 𝕜 → E}, MeromorphicAt f x → (MeromorphicAt (f - g) x ↔ MeromorphicAt g x)
-- Mathlib.FieldTheory.AlgebraicClosure
/-- If `K / E / F` is a field extension tower, such that `E / F` is algebraic, then
`algebraicClosure F K` is equal to `algebraicClosure E K`.  -/
algebraicClosure.eq_restrictScalars_of_isAlgebraic : ∀ (F : Type u_1) (E : Type u_2) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type u_3)
  [inst_3 : Field K] [inst_4 : Algebra F K] [inst_5 : Algebra E K] [inst_6 : IsScalarTower F E K]
  [Algebra.IsAlgebraic F E], algebraicClosure F K = IntermediateField.restrictScalars F (algebraicClosure E K)
-- Mathlib.CategoryTheory.FiberedCategory.Fiber
CategoryTheory.Functor.Fiber.inducedFunctor_comp_map : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  {p : CategoryTheory.Functor 𝒳 𝒮} {S : 𝒮} {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor C 𝒳} (hF : F.comp p = (CategoryTheory.Functor.const C).obj S) {X Y : C} (f : X ⟶ Y),
  CategoryTheory.Functor.Fiber.fiberInclusion.map ((CategoryTheory.Functor.Fiber.inducedFunctor hF).map f) = F.map f
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.instReprLeapSecond : Repr Std.Time.TimeZone.TZif.LeapSecond
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.mem_union_of_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α}, k ∈ t₂ → k ∈ t₁ ∪ t₂
-- Std.Time.Notation
_private.Std.Time.Notation.0.Std.Time.convertFraction : Std.Time.Fraction → Lean.MacroM (Lean.TSyntax `term)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.natCast_def : ∀ {k : Type u_1} {G : Type u_2} [inst : One G] [inst_1 : AddMonoidWithOne k] (n : ℕ), ↑n = SkewMonoidAlgebra.single 1 ↑n
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.image_vadd_product : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] {s : Finset α} {t : Finset β},
  Finset.image (fun x => x.1 +ᵥ x.2) (s ×ˢ t) = s +ᵥ t
-- Mathlib.Order.Interval.Set.OrderIso
OrderIso.image_Ici : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β) (a : α),
  ⇑e '' Set.Ici a = Set.Ici (e a)
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.minKeyD.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : Std.DTreeMap.Internal.Impl α β → α → Sort u_3) →
      (x : Std.DTreeMap.Internal.Impl α β) →
        (x_1 : α) →
          ((fallback : α) → motive Std.DTreeMap.Internal.Impl.leaf fallback) →
            ((size : ℕ) →
                (k : α) →
                  (v : β k) →
                    (r : Std.DTreeMap.Internal.Impl α β) →
                      (x : α) →
                        motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x) →
              ((size : ℕ) →
                  (k : α) →
                    (v : β k) →
                      (size_1 : ℕ) →
                        (k_1 : α) →
                          (v_1 : β k_1) →
                            (l r r_1 : Std.DTreeMap.Internal.Impl α β) →
                              (fallback : α) →
                                motive
                                  (Std.DTreeMap.Internal.Impl.inner size k v
                                    (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1)
                                  fallback) →
                motive x x_1
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.instCartesianMonoidalCategory : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] → CategoryTheory.CartesianMonoidalCategory (CategoryTheory.AddGrp C)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.size_filterMap_le_size : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp}
  [Std.TransCmp cmp] {f : (a : α) → β a → Option (γ a)}, t.WF → (Std.DTreeMap.Raw.filterMap f t).size ≤ t.size
-- Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
NumberField.isTotallyComplex_of_algebra : ∀ (F : Type u_1) [inst : Field F] (K : Type u_2) [inst_1 : Field K] [Algebra F K] [NumberField.IsTotallyComplex F],
  NumberField.IsTotallyComplex K
-- Init.Data.Float.Model.Unpacked.Sign
Float.Model.UnpackedFloat.Sign.noConfusionType : Sort v✝ → Float.Model.UnpackedFloat.Sign → Float.Model.UnpackedFloat.Sign → Sort v✝
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.Tendsto.sub : ∀ {α : Type u_1} {f : Filter α} {ma mb : α → ENNReal} {a b : ENNReal},
  Filter.Tendsto ma f (nhds a) →
    Filter.Tendsto mb f (nhds b) → a ≠ ⊤ ∨ b ≠ ⊤ → Filter.Tendsto (fun a => ma a - mb a) f (nhds (a - b))
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.fvarsSizeLtMaxFVars : Array Lean.Expr → Option ℕ → Bool
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.toPiLocalizationEquiv_apply : ∀ (R : Type u) [inst : CommSemiring R] [inst_1 : DiscreteTopology (PrimeSpectrum R)] (x : R),
  (PrimeSpectrum.toPiLocalizationEquiv R) x = (algebraMap R (PrimeSpectrum.PiLocalization R)) x
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.nonempty_neighborSet : ∀ {V : Type u} {G : SimpleGraph V} {v : V}, (G.neighborSet v).Nonempty ↔ ∃ u, G.Adj v u
-- Mathlib.Analysis.RCLike.Basic
RCLike.lipschitzWith_im : ∀ {K : Type u_1} [inst : RCLike K], LipschitzWith 1 ⇑RCLike.im
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.CliqueFreeOn.mono : ∀ {α : Type u_1} (G : SimpleGraph α) {s : Set α} {m n : ℕ}, m ≤ n → G.CliqueFreeOn s m → G.CliqueFreeOn s n
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.Comma.preservesColimitsOfShape_snd : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {A : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} A]
  {B : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃}
  [inst_3 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T}
  [CategoryTheory.Limits.HasColimitsOfShape J A] [CategoryTheory.Limits.HasColimitsOfShape J B]
  [CategoryTheory.Limits.PreservesColimitsOfShape J L],
  CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.Comma.snd L R)
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
TendstoUniformly.div : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Type u_3}
  {l : Filter ι} {f f' : ι → β → α} {g g' : β → α},
  TendstoUniformly f g l → TendstoUniformly f' g' l → TendstoUniformly (f / f') (g / g') l
-- Init.Data.Vector.Algebra
Vector.getElem_smul : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} [inst : SMul α β] (c : α) (xs : Vector β n) (i : ℕ) (h : i < n),
  (c • xs)[i] = c • xs[i]
-- Mathlib.Algebra.Order.Group.OrderIso
OrderIso.addLeft_apply : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [inst_2 : AddLeftMono α] (a x : α), (OrderIso.addLeft a) x = a + x
-- Mathlib.GroupTheory.GroupAction.Blocks
MulAction.IsBlockSystem.eq_1 : ∀ (G : Type u_1) [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] (ℬ : Set (Set X)),
  MulAction.IsBlockSystem G ℬ = (Setoid.IsPartition ℬ ∧ ∀ ⦃B : Set X⦄, B ∈ ℬ → MulAction.IsBlock G B)
-- Init.Prelude
/-- The first element of a pair.  -/
Prod.fst : {α : Type u} → {β : Type v} → α × β → α
-- Lean.Elab.Config
/-- Set `isDefEq` configuration for the elaborator.
Note that we enable all approximations but `quasiPatternApprox`

In Lean3 and Lean 4, we used to use the quasi-pattern approximation during elaboration.
The example:
```
def ex : StateT δ (StateT σ Id) σ :=
monadLift (get : StateT σ Id σ)
```
demonstrates why it produces counterintuitive behavior.
We have the `Monad-lift` application:
```
@monadLift ?m ?n ?c ?α (get : StateT σ id σ) : ?n ?α
```
It produces the following unification problem when we process the expected type:
```
?n ?α =?= StateT δ (StateT σ id) σ
==> (approximate using first-order unification)
?n := StateT δ (StateT σ id)
?α := σ
```
Then, we need to solve:
```
?m ?α =?= StateT σ id σ
==> instantiate metavars
?m σ =?= StateT σ id σ
==> (approximate since it is a quasi-pattern unification constraint)
?m := fun σ => StateT σ id σ
```
Note that the constraint is not a Milner pattern because σ is in
the local context of `?m`. We are ignoring the other possible solutions:
```
?m := fun σ' => StateT σ id σ
?m := fun σ' => StateT σ' id σ
?m := fun σ' => StateT σ id σ'
```

We need the quasi-pattern approximation for elaborating recursor-like expressions (e.g., dependent `match with` expressions).

If we had use first-order unification, then we would have produced
the right answer: `?m := StateT σ id`

Haskell would work on this example since it always uses
first-order unification.
 -/
Lean.Elab.Term.setElabConfig : Lean.Meta.Config → Lean.Meta.Config
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.evalAlts : Lean.Meta.ElimInfo →
  Array Lean.Elab.Tactic.ElimApp.Alt →
    Lean.Syntax →
      Option (Array Lean.Syntax) →
        Lean.Elab.Tactic.TacticM Lean.Elab.Info →
          Lean.Syntax →
            optParam ℕ 0 →
              optParam (Array Lean.FVarId) #[] →
                optParam (Array Lean.FVarId) #[] →
                  optParam (Array (Lean.Ident × Lean.FVarId)) #[] → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
/-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
because it is a composition of multiple projections.  -/
BoundedContinuousFunction.Simps.apply : {α : Type u} →
  {β : Type v} → [inst : TopologicalSpace α] → [inst_1 : PseudoMetricSpace β] → BoundedContinuousFunction α β → α → β
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPolynomial.coe_C : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (a : R), ↑(MvPolynomial.C a) = MvPowerSeries.C a
-- Mathlib.Data.FunLike.IsApply
/-- **Alias** of `IsAddApply.add_apply`. -/
add_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Add β}
  {inst_2 : Add F} [self : IsAddApply F α β] (f g : F) (x : α), (f + g) x = f x + g x
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CtorInfo.cidx : Lean.Compiler.LCNF.CtorInfo → ℕ
-- Mathlib.Data.Nat.Choose.Basic
Nat.choose_symm : ∀ {n k : ℕ}, k ≤ n → n.choose (n - k) = n.choose k
-- Mathlib.Combinatorics.Matroid.IndepAxioms
Matroid.ofExistsMatroid_E : ∀ {α : Type u_1} (E : Set α) (Indep : Set α → Prop) (hM : ∃ M, E = M.E ∧ ∀ (I : Set α), M.Indep I ↔ Indep I),
  (Matroid.ofExistsMatroid E Indep hM).E = E
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.iIndep_precomp_of_bijective : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {m : ι → MeasurableSpace Ω}
  {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {ι' : Type u_5}
  {g : ι' → ι},
  Function.Bijective g → (ProbabilityTheory.Kernel.iIndep (m ∘ g) κ μ ↔ ProbabilityTheory.Kernel.iIndep m κ μ)
-- Mathlib.GroupTheory.GroupAction.Quotient
AddAction.Quotient.vadd_mk : ∀ {G : Type u} {X : Type v} [inst : AddGroup G] [inst_1 : AddMonoid X] [inst_2 : AddAction X G] (H : AddSubgroup G)
  [inst_3 : AddAction.QuotientAction X H] (b : X) (g : G), b +ᵥ ↑g = ↑(b +ᵥ g)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas
aestronglyMeasurable_withDensity_iff : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_4} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {f : α → NNReal},
  Measurable f →
    ∀ {g : α → E},
      MeasureTheory.AEStronglyMeasurable g (μ.withDensity fun x => ↑(f x)) ↔
        MeasureTheory.AEStronglyMeasurable (fun x => ↑(f x) • g x) μ
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.AECover.ae_tendsto_indicator : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι} {β : Type u_3}
  [inst_1 : Zero β] [inst_2 : TopologicalSpace β] (f : α → β) {φ : ι → Set α},
  MeasureTheory.AECover μ l φ → ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun i => (φ i).indicator f x) l (nhds (f x))
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.Context.mk : Lean.Options → Lean.Parser.TokenTable → Lean.PrettyPrinter.Formatter.Context
-- Mathlib.LinearAlgebra.Basis.VectorSpace
LinearMap.exists_leftInverse_of_injective : ∀ {K : Type u_3} {V : Type u_4} {V' : Type u_5} [inst : DivisionRing K] [inst_1 : AddCommGroup V]
  [inst_2 : AddCommGroup V'] [inst_3 : Module K V] [inst_4 : Module K V'] (f : V →ₗ[K] V'),
  f.ker = ⊥ → ∃ g, g ∘ₗ f = LinearMap.id
-- Mathlib.Combinatorics.SetFamily.Shadow
/-- `t ∈ ∂^k 𝒜` iff `t` is exactly `k` elements less than something from `𝒜`.

See also `Finset.mem_shadow_iff_exists_mem_card_add`.  -/
Finset.mem_shadow_iterate_iff_exists_sdiff : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {t : Finset α} {k : ℕ},
  t ∈ Finset.shadow^[k] 𝒜 ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ (s \ t).card = k
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.mono_homMk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T : CategoryTheory.Functor C D} {A B : CategoryTheory.StructuredArrow S T} (f : A.right ⟶ B.right)
  (w : CategoryTheory.CategoryStruct.comp A.hom (T.map f) = B.hom) [h : CategoryTheory.Mono f],
  CategoryTheory.Mono (CategoryTheory.StructuredArrow.homMk f w)
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.instPow.eq_1 : ∀ {ι : Type u_1} {α : Type u_2} {M : ι → Type u_5} [inst : (i : ι) → Pow (M i) α],
  Pi.instPow = { pow := fun f a i => f i ^ a }
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.ToForwardSearcher.DefaultForwardSearcher.instIteratorIdSearchStepOfForwardPattern : {ρ : Type} →
  (pat : ρ) →
    (s : String.Slice) →
      [String.Slice.Pattern.ForwardPattern pat] →
        Std.Iterator (String.Slice.Pattern.ToForwardSearcher.DefaultForwardSearcher pat s) Id
          (String.Slice.Pattern.SearchStep s)
-- Mathlib.Probability.Kernel.Category.SFinKer
SFinKer.str : (self : SFinKer) → MeasurableSpace self.carrier
-- Init.Data.Array.Basic
Array.size_swap : ∀ {α : Type u} {xs : Array α} {i j : ℕ} {hi : i < xs.size} {hj : j < xs.size}, (xs.swap i j hi hj).size = xs.size
-- Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toBiprod_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] [inst_2 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_3 : CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] (S : J.MayerVietorisSquare)
  (F : CategoryTheory.Sheaf J AddCommGrpCat) {n : ℕ} (y : ↑(F.H' n S.X₄)),
  (CategoryTheory.ConcreteCategory.hom (S.toBiprod F n)) y =
    (CategoryTheory.ConcreteCategory.hom
        (((F.cohomologyPresheaf n).obj (Opposite.op S.X₂)).biprodIsoProd
            ((F.cohomologyPresheaf n).obj (Opposite.op S.X₃))).inv)
      ((CategoryTheory.ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₂₄.op)) y,
        (CategoryTheory.ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₃₄.op)) y)
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
analyticAt_sigmoid : ∀ {x : ℝ}, AnalyticAt ℝ Real.sigmoid x
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_cast_Ici : ∀ {m n : ℕ} (h : m = n) (i : Fin n), Fin.cast h ⁻¹' Set.Ici i = Set.Ici (Fin.cast ⋯ i)
-- Mathlib.Algebra.Order.Ring.WithTop
RingHom.withTopMap_apply : ∀ {R : Type u_2} {S : Type u_3} [inst : NonAssocSemiring R] [inst_1 : PartialOrder R] [inst_2 : CanonicallyOrderedAdd R]
  [inst_3 : DecidableEq R] [inst_4 : Nontrivial R] [inst_5 : NonAssocSemiring S] [inst_6 : PartialOrder S]
  [inst_7 : CanonicallyOrderedAdd S] [inst_8 : DecidableEq S] [inst_9 : Nontrivial S] (f : R →+* S)
  (hf : Function.Injective ⇑f), ⇑(f.withTopMap hf) = (↑(f.toMonoidWithZeroHom.withTopMap hf)).toFun
-- Mathlib.CategoryTheory.Functor.ReflectsIso.Basic
CategoryTheory.reflectsIsomorphisms_comp : ∀ {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 : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [F.ReflectsIsomorphisms] [G.ReflectsIsomorphisms],
  (F.comp G).ReflectsIsomorphisms
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.map_map : ∀ {I : Type u_1} {J : Type u_2} (C : Type u_4) [inst : CategoryTheory.Category.{v_1, u_4} C] (p : I → J)
  [inst_1 : ∀ (j : J), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete ↑(p ⁻¹' {j})) C]
  {X Y : CategoryTheory.GradedObject I C} (φ : X ⟶ Y) (i : J),
  (CategoryTheory.GradedObject.map C p).map φ i = CategoryTheory.GradedObject.mapMap φ p i
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.presieve₀_restrictIndex_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) {ι : Type u_1}
  (f : ι → E.I₀), (E.restrictIndex f).presieve₀ ≤ E.presieve₀
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get!_union : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α} [inst_1 : Inhabited (β k)], (t₁ ∪ t₂).get! k = t₂.getD k (t₁.get! k)
-- Mathlib.Analysis.Complex.Convex
/-- The slit plane is star-shaped at a positive real number.  -/
Complex.starConvex_ofReal_slitPlane : ∀ {x : ℝ}, 0 < x → StarConvex ℝ (↑x) Complex.slitPlane
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.insertMany.congr_simp : ∀ {α : Type u} {β : Type v} [inst : Ord α] {ρ : Type w} [inst_1 : ForIn Id ρ (α × β)]
  (t : Std.DTreeMap.Internal.Impl α fun x => β) (l l_1 : ρ),
  l = l_1 →
    ∀ (h : t.Balanced),
      Std.DTreeMap.Internal.Impl.Const.insertMany t l h = Std.DTreeMap.Internal.Impl.Const.insertMany t l_1 h
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
CategoryTheory.Functor.mapExtLinearMap_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.Additive] [inst_5 : CategoryTheory.Limits.PreservesFiniteLimits F]
  [inst_6 : CategoryTheory.Limits.PreservesFiniteColimits F] [inst_7 : CategoryTheory.HasExt C]
  [inst_8 : CategoryTheory.HasExt D] (X Y : C) (n : ℕ) (R : Type u_1) [inst_9 : Ring R]
  [inst_10 : CategoryTheory.Linear R C] [inst_11 : CategoryTheory.Linear R D]
  [inst_12 : CategoryTheory.Functor.Linear R F] (e : CategoryTheory.Abelian.Ext X Y n),
  (F.mapExtLinearMap R X Y n) e = CategoryTheory.Abelian.Ext.mapExactFunctor F e
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey!_diff : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {k : α},
  (m₁ \ m₂).getKey! k = if k ∈ m₂ then default else m₁.getKey! k
-- Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain
HasStrictFDerivAt.hasStrictFDerivAt_implicitFunctionOfProdDomain : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E₁ : Type u_2} [inst_1 : NormedAddCommGroup E₁]
  [inst_2 : NormedSpace 𝕜 E₁] [inst_3 : CompleteSpace E₁] {E₂ : Type u_3} [inst_4 : NormedAddCommGroup E₂]
  [inst_5 : NormedSpace 𝕜 E₂] [inst_6 : CompleteSpace E₂] {F : Type u_4} [inst_7 : NormedAddCommGroup F]
  [inst_8 : NormedSpace 𝕜 F] [inst_9 : CompleteSpace F] {u : E₁ × E₂} {f : E₁ × E₂ → F} {f'u : E₁ × E₂ →L[𝕜] F}
  (dfu : HasStrictFDerivAt f f'u u) (if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible),
  HasStrictFDerivAt (dfu.implicitFunctionOfProdDomain if₂u)
    (-(f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).inverse ∘SL f'u ∘SL ContinuousLinearMap.inl 𝕜 E₁ E₂) u.1
-- Mathlib.NumberTheory.NumberField.House
_private.Mathlib.NumberTheory.NumberField.House.0.NumberField.house.c₂.eq_1 : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] [inst_2 : DecidableEq (K →+* ℂ)],
  NumberField.house.c₂✝ K = max 1 (NumberField.house.c✝ K) * NumberField.house.supOfBasis✝ K
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.constantCoeff_subst_eq_zero : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {a : σ → MvPowerSeries τ S},
  MvPowerSeries.HasSubst a →
    (∀ (i : σ), MvPowerSeries.constantCoeff (a i) = 0) →
      ∀ {f : MvPowerSeries σ R},
        MvPowerSeries.constantCoeff f = 0 → MvPowerSeries.constantCoeff (MvPowerSeries.subst a f) = 0
-- Lean.Meta.AppBuilder
/-- Similar to `mkAppM`, but it allows us to specify which arguments are provided explicitly using `Option` type.
Example:
Given `Pure.pure {m : Type u → Type v} [Pure m] {α : Type u} (a : α) : m α`,
```
mkAppOptM `Pure.pure #[m, none, none, a]
```
returns a `Pure.pure` application if the instance `Pure m` can be synthesized, and the universe match.
Note that,
```
mkAppM `Pure.pure #[a]
```
fails because the only explicit argument `(a : α)` is not sufficient for inferring the remaining arguments,
we would need the expected type.  -/
Lean.Meta.mkAppOptM : Lean.Name → Array (Option Lean.Expr) → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.Sites.Over
/-- **Alias** of `TopHomClass.map_top`. -/
CategoryTheory.Sieve.overEquiv_symm_top : ∀ {F : Type u_6} {α : outParam (Type u_7)} {β : outParam (Type u_8)} {inst : Top α} {inst_1 : Top β}
  {inst_2 : FunLike F α β} [self : TopHomClass F α β] (f : F), f ⊤ = ⊤
-- Mathlib.CategoryTheory.Sigma.Basic
CategoryTheory.Sigma.inclDesc_hom_app : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (F : (i : I) → CategoryTheory.Functor (C i) D) (i : I) (X : C i),
  (CategoryTheory.Sigma.inclDesc F i).hom.app X = CategoryTheory.CategoryStruct.id ((F i).obj X)
-- Mathlib.Topology.Algebra.Group.Defs
/-- Eta-expanded form of `ContinuousOn.sub` -/
ContinuousOn.fun_sub : ∀ {G : Type u_1} {X : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace G] [inst_2 : Sub G]
  [ContinuousSub G] {f g : X → G} {s : Set X}, ContinuousOn f s → ContinuousOn g s → ContinuousOn (fun i => f i - g i) s
-- Init.Data.Array.MapIdx
List.mapFinIdxM.go.eq_2 : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (as : List α)
  (f : (i : ℕ) → α → i < as.length → m β) (acc : Array β) (a : α) (as_1 : List α)
  (a_1 : (a :: as_1).length + acc.size = as.length),
  List.mapFinIdxM.go as f (a :: as_1) acc a_1 = do
    let __do_lift ← f acc.size a ⋯
    List.mapFinIdxM.go as f as_1 (acc.push __do_lift) ⋯
-- Mathlib.Data.Set.SMulAntidiagonal
Set.SMulAntidiagonal.eq_of_fst_le_fst_of_snd_le_snd : ∀ {G : Type u_1} {P : Type u_2} {s : Set G} {t : Set P} {a : P} [inst : PartialOrder G] [inst_1 : PartialOrder P]
  [inst_2 : SMul G P] [IsOrderedCancelSMul G P] {x y : ↑(s.smulAntidiagonal t a)},
  (↑x).1 ≤ (↑y).1 → (↑x).2 ≤ (↑y).2 → x = y