mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.map_ofArrows : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {X : C} {ι : Type u_1} {Y : ι → C} (f : (i : ι) → Y i ⟶ X),
  CategoryTheory.Presieve.map F (CategoryTheory.Presieve.ofArrows Y f) =
    CategoryTheory.Presieve.ofArrows (fun i => F.obj (Y i)) fun i => F.map (f i)
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.not_insert_eq_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α}, ¬m.insert k = ∅
-- Mathlib.Analysis.InnerProductSpace.ExteriorPower
_private.Mathlib.Analysis.InnerProductSpace.ExteriorPower.0.exteriorPower.innerProductForm_self : ∀ {n : ℕ} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] (x : ↥(⋀[ℝ]^n E)) {ι : Type u_2}
  [inst_2 : Fintype ι] [inst_3 : LinearOrder ι] (b : OrthonormalBasis ι ℝ E),
  (exteriorPower.innerProductForm✝ x) x = ∑ s, ((Module.Basis.exteriorPower n b.toBasis).repr x) s ^ 2
-- Mathlib.Topology.Homotopy.Product
/-- Lemmas showing projection is the inverse of product.  -/
Path.Homotopic.projLeft_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {a₁ a₂ : α} {b₁ b₂ : β}
  (q₁ : Path.Homotopic.Quotient a₁ a₂) (q₂ : Path.Homotopic.Quotient b₁ b₂),
  Path.Homotopic.projLeft (Path.Homotopic.prod q₁ q₂) = q₁
-- Mathlib.Data.PFun
PFun.fixInduction'_fwd : ∀ {α : Type u_1} {β : Type u_2} {C : α → Sort u_7} {f : α →. β ⊕ α} {b : β} {a a' : α} (h : b ∈ f.fix a)
  (h' : b ∈ f.fix a') (fa : Sum.inr a' ∈ f a) (hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final)
  (hind : (a₀ a₁ : α) → b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀),
  PFun.fixInduction' h hbase hind = hind a a' h' fa (PFun.fixInduction' h' hbase hind)
-- Lean.MetavarContext
/-- `isWellFormed lctx e` returns true iff
- All locals in `e` are declared in `lctx`
- All metavariables `?m` in `e` have a local context which is a subprefix of `lctx` or are assigned, and the assignment is well-formed.  -/
Lean.MetavarContext.isWellFormed : {m : Type → Type} → [Monad m] → [Lean.MonadMCtx m] → Lean.LocalContext → Lean.Expr → m Bool
-- Mathlib.Data.Fintype.Defs
/-- Given a predicate that can be represented by a finset, the subtype
associated to the predicate is a fintype.  -/
Fintype.subtype : {α : Type u_1} → {p : α → Prop} → (s : Finset α) → (∀ (x : α), x ∈ s ↔ p x) → Fintype { x // p x }
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.exists_of_eRank_eq_zero : ∀ {α : Type u_1} {M : Matroid α}, M.eRank = 0 → ∃ X, M = Matroid.loopyOn X
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_castAddEmb_Ioo : ∀ {n : ℕ} (m : ℕ) (i j : Fin n),
  Finset.map (Fin.castAddEmb m) (Finset.Ioo i j) = Finset.Ioo (Fin.castAdd m i) (Fin.castAdd m j)
-- Mathlib.Data.Nat.Init
/-- A version of `Nat.div_lt_self` using successors, rather than additional hypotheses.  -/
Nat.div_lt_self' : ∀ (a b : ℕ), (a + 1) / (b + 2) < a + 1
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.denote_le_cancelAux : ∀ (ctx : Nat.Internal.Linear.Context) (fuel : ℕ) (m₁ m₂ r₁ r₂ : Nat.Internal.Linear.Poly),
  Nat.Internal.Linear.Poly.denote_le ctx (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂) →
    Nat.Internal.Linear.Poly.denote_le ctx (Nat.Internal.Linear.Poly.cancelAux fuel m₁ m₂ r₁ r₂)
-- Mathlib.Data.List.AList
AList.entries_insert : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {b : β a} {s : AList β},
  (AList.insert a b s).entries = ⟨a, b⟩ :: List.kerase a s.entries
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_congr : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {f g : R → R} {a : A},
  Set.EqOn f g (spectrum R a) → cfc f a = cfc g a
-- Mathlib.Order.Interval.Finset.Basic
/-- **Alias** of `Finset.Icc_sdiff_both`. -/
Finset.Icc_diff_both : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : DecidableEq α] (a b : α),
  Finset.Icc a b \ {a, b} = Finset.Ioo a b
-- Mathlib.Analysis.Fourier.AddCircleMulti
UnitAddTorus.mFourier.eq_1 : ∀ {d : Type u_1} [inst : Fintype d] (n : d → ℤ),
  UnitAddTorus.mFourier n = { toFun := fun x => ∏ i, (fourier (n i)) (x i), continuous_toFun := ⋯ }
-- Mathlib.Data.Set.Finite.Lattice
Set.map_finite_iInf : ∀ {α : Type u} {β : Type v} {F : Type u_1} {ι : Type u_2} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  [inst_2 : FunLike F α β] [InfTopHomClass F α β] [Finite ι] (f : F) (g : ι → α), f (⨅ i, g i) = ⨅ i, f (g i)
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
ContinuousLinearMap.inl.eq_1 : ∀ (R : Type u_1) [inst : Semiring R] (M₁ : Type u_2) [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R M₁] (M₂ : Type u_3) [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂], ContinuousLinearMap.inl R M₁ M₂ = (ContinuousLinearMap.id R M₁).prod 0
-- Mathlib.Data.Nat.Factorization.Basic
Nat.prod_primeFactors_gcd_mul_prod_primeFactors_mul : ∀ {β : Type u_1} [inst : CommMonoid β] (m n : ℕ) (f : ℕ → β),
  (m.gcd n).primeFactors.prod f * (m * n).primeFactors.prod f = m.primeFactors.prod f * n.primeFactors.prod f
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.getChildNgen : {M : Type → Type} → [Monad M] → [Lean.MonadNameGenerator M] → M Lean.NameGenerator
-- Mathlib.Data.DFinsupp.Order
DFinsupp.support_monotone : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → AddCommMonoid (α i)] [inst_1 : (i : ι) → PartialOrder (α i)]
  [∀ (i : ι), CanonicallyOrderedAdd (α i)] [inst_3 : DecidableEq ι] [inst_4 : (i : ι) → (x : α i) → Decidable (x ≠ 0)],
  Monotone DFinsupp.support
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- the symmetry isomorphism  -/
CategoryTheory.Limits.MultispanIndex.SymmStruct.iso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {ι : Type w} →
      {I : CategoryTheory.Limits.MultispanIndex (CategoryTheory.Limits.MultispanShape.prod ι) C} →
        I.SymmStruct → (i j : ι) → I.left (i, j) ≅ I.left (j, i)
-- Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
CoalgCat.MonoidalCategoryAux.rightUnitor_hom_toLinearMap : ∀ {R : Type u} [inst : CommRing R] {M : Type u} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : Coalgebra R M],
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CoalgCat.of R M)).hom.toCoalgHom'.toLinearMap =
    ↑(TensorProduct.rid R M)
-- Mathlib.GroupTheory.Complement
AddSubgroup.IsComplement.ncard_left : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {S : Set G}, AddSubgroup.IsComplement S ↑H → S.ncard = H.index
-- Mathlib.LinearAlgebra.DFinsupp
/-- Independence of a family of submodules can be expressed as a quantifier over `DFinsupp`s.

This is an intermediate result used to prove
`iSupIndep_of_dfinsupp_lsum_injective` and
`iSupIndep.dfinsupp_lsum_injective`.  -/
iSupIndep_iff_forall_dfinsupp : ∀ {ι : Type u_1} {R : Type u_3} {N : Type u_6} [inst : DecidableEq ι] [inst_1 : Semiring R] [inst_2 : AddCommMonoid N]
  [inst_3 : Module R N] (p : ι → Submodule R N),
  iSupIndep p ↔
    ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)),
      ((DFinsupp.lsum ℕ) fun i => (p i).subtype) (DFinsupp.erase i v) = ↑x → x = 0
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {a fallback : α}, t.isEmpty = true → t.getKeyD a fallback = fallback
-- Mathlib.Algebra.Group.Defs
/-- A `DivInvMonoid` where `1⁻¹ = 1`.  -/
DivInvOneMonoid : Type u_2 → Type u_2
-- Mathlib.Order.SuccPred.Basic
WithBot.pred_coe_of_isMin : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] [inst_2 : (a : α) → Decidable (Order.pred a = a)]
  {a : α}, IsMin a → Order.pred ↑a = ⊥
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.instHashableExtraTheorem : Hashable Lean.Elab.Tactic.Grind.ExtraTheorem
-- Mathlib.Topology.Algebra.Group.Defs
/-- Eta-expanded form of `ContinuousOn.inv` -/
ContinuousOn.fun_inv : ∀ {G : Type u_1} {X : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace G] [inst_2 : Inv G]
  [ContinuousInv G] {f : X → G} {s : Set X}, ContinuousOn f s → ContinuousOn (fun i => (f i)⁻¹) s
-- Mathlib.Data.Nat.Prime.Basic
/-- If `0 < m < minFac n`, then `n` and `m` have gcd equal to `1`.  -/
Nat.gcd_eq_one_of_lt_minFac : ∀ {n m : ℕ}, m ≠ 0 → m < n.minFac → n.gcd m = 1
-- Init.Data.Vector.Lemmas
Vector.getElem_eq_getElem?_get : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} (h : i < n), xs[i] = xs[i]?.get ⋯
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.SymbolicBound.ival? : Lean.Meta.Grind.Arith.Cutsat.SymbolicBound → Option ℤ
-- Init.Data.Repr
instReprList : {α : Type u_1} → [Repr α] → Repr (List α)
-- Mathlib.Order.Hom.Lex
OrderIso.sumLexIicIoi_symm_apply_Ioi : ∀ {α : Type u_1} [inst : LinearOrder α] {x : α} (a : ↑(Set.Ioi x)), (OrderIso.sumLexIicIoi x).symm ↑a = Sum.inr a
-- Mathlib.Algebra.GCDMonoid.Basic
gcd_mul_right : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : StrongNormalizedGCDMonoid α] (a b c : α),
  gcd (b * a) (c * a) = gcd b c * normalize a
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
ProfiniteAddGrp.toLimit_injective : ∀ (P : ProfiniteAddGrp.{u}), Function.Injective ⇑(ProfiniteAddGrp.Hom.hom P.toLimit)
-- Mathlib.RepresentationTheory.Homological.TateCohomology.Basic
Rep.norm_comp_d_eq_zero_assoc : ∀ {R G : Type u} [inst : CommRing R] [inst_1 : Group G] [inst_2 : Fintype G] (M : Rep.{max u u_1, u, u} R G)
  {Z : ModuleCat R} (h : ModuleCat.of R (G → ↑M) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (Rep.Hom.toModuleCatHom M.norm)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.d₀₁ M) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- The quotient `G ⧸ N` of a complete first countable topological group `G` by a normal subgroup
is itself complete. [N. Bourbaki, *General Topology*, IX.3.1 Proposition 4][bourbaki1966b]

Because a topological group is not equipped with a `UniformSpace` instance by default, we must
explicitly provide it in order to consider completeness. See `QuotientGroup.completeSpace_left` for
a version in which `G` is already equipped with a uniform structure.  -/
QuotientGroup.completeSpace_left' : ∀ (G : Type u) [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G] [FirstCountableTopology G]
  (N : Subgroup G) [inst_4 : N.Normal] [hG : CompleteSpace G], CompleteSpace (G ⧸ N)
-- Mathlib.AlgebraicTopology.SimplicialObject.II
SimplexCategory.II.map'_map' : ∀ {n m p : ℕ} (f : Fin (n + 1) →o Fin (m + 1)) (g : Fin (m + 1) →o Fin (p + 1)) (x : Fin (p + 2)),
  SimplexCategory.II.map' f (SimplexCategory.II.map' g x) = SimplexCategory.II.map' (g.comp f) x
-- Mathlib.Tactic.IntervalCases
Mathlib.Tactic.IntervalCases.IntervalCasesSubgoal.mk.sizeOf_spec : ∀ (rhs : Lean.Expr) (value : ℤ) (goal : Lean.MVarId),
  sizeOf { rhs := rhs, value := value, goal := goal } = 1 + sizeOf rhs + sizeOf value + sizeOf goal
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.isoMk_inv_left : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {L₁ : CategoryTheory.Functor A T}
  {R₁ : CategoryTheory.Functor B T} {X Y : CategoryTheory.Comma L₁ R₁} (l : X.left ≅ Y.left) (r : X.right ≅ Y.right)
  (h :
    autoParam
      (CategoryTheory.CategoryStruct.comp (L₁.map l.hom) Y.hom =
        CategoryTheory.CategoryStruct.comp X.hom (R₁.map r.hom))
      CategoryTheory.Comma.isoMk._auto_1),
  (CategoryTheory.Comma.isoMk l r h).inv.left = l.inv
-- Mathlib.Order.Hom.Bounded
BotHom.instLE.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Bot α] [inst_1 : LE β] [inst_2 : Bot β],
  BotHom.instLE = { le := fun g f => ⇑g ≤ ⇑f }
-- Lean.Server.FileWorker.InlayHints
Lean.Elab.InlayHintLabelPart.toLspInlayHintLabelPart : Lean.FileMap → Lean.Elab.InlayHintLabelPart → IO Lean.Lsp.InlayHintLabelPart
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.HasModel.mk : {α : Type u} →
  [inst : LE α] →
    [inst_1 : LT α] →
      {β : outParam (Type v)} →
        [inst_2 : LE β] →
          [inst_3 : LT β] →
            [inst_4 : Std.PRange.UpwardEnumerable β] →
              [inst_5 : Std.PRange.LawfulUpwardEnumerable β] →
                [inst_6 : Std.PRange.LawfulUpwardEnumerableLE β] →
                  [inst_7 : Std.PRange.LawfulUpwardEnumerableLT β] →
                    (encode : α → β) →
                      (decode : β → α) →
                        (∀ {x : β}, encode (decode x) = x) →
                          (∀ {x : α}, decode (encode x) = x) →
                            (∀ {x y : α}, x ≤ y ↔ encode x ≤ encode y) →
                              (∀ {x y : α}, x < y ↔ encode x < encode y) → HasModel✝ α β
-- Mathlib.GroupTheory.PGroup
IsPGroup.to_le : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] {H K : Subgroup G}, IsPGroup p ↥K → H ≤ K → IsPGroup p ↥H
-- Mathlib.MeasureTheory.Measure.MeasuredSets
MeasureTheory.instPseudoMetricSpaceMeasuredSetsOfIsFiniteMeasure : {α : Type u_1} →
  [mα : MeasurableSpace α] →
    {μ : MeasureTheory.Measure α} → [MeasureTheory.IsFiniteMeasure μ] → PseudoMetricSpace (MeasureTheory.MeasuredSets μ)
-- Mathlib.AlgebraicTopology.SimplexCategory.Rev
SimplexCategory.rev_map_apply : ∀ {n m : SimplexCategory} (f : n ⟶ m) (i : Fin (n.len + 1)),
  (SimplexCategory.Hom.toOrderHom (SimplexCategory.rev.map f)) i = ((SimplexCategory.Hom.toOrderHom f) i.rev).rev
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.mk.sizeOf_spec : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero X] [inst_1 : Zero R] [inst_2 : TopologicalSpace X]
  [inst_3 : TopologicalSpace R] [inst_4 : SizeOf X] [inst_5 : SizeOf R] (toContinuousMap : C(X, R))
  (map_zero' : toContinuousMap 0 = 0),
  sizeOf { toContinuousMap := toContinuousMap, map_zero' := map_zero' } = 1 + sizeOf toContinuousMap + sizeOf map_zero'
-- Mathlib.Data.EReal.Inv
EReal.instDivInvMonoid : DivInvMonoid EReal
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.processNonVariable : Lean.Meta.Match.Problem → Lean.MetaM Lean.Meta.Match.Problem
-- Init.Data.UInt.IntToBitVec
USize.toBitVec64_div : ∀ {a b : USize} (h : System.Platform.numBits = 64), (a / b).toBitVec64 h = a.toBitVec64 h / b.toBitVec64 h
-- Init.Data.Int.Order
Int.lt_succ : ∀ (a : ℤ), a < a + 1
-- Mathlib.Combinatorics.Enumerative.Composition
_private.Mathlib.Combinatorics.Enumerative.Composition.0.List.splitWrtCompositionAux.match_1.splitter : {α : Type u_1} →
  (motive : List α × List α → Sort u_2) → (x : List α × List α) → ((l₁ l₂ : List α) → motive (l₁, l₂)) → motive x
-- Mathlib.Order.WellFoundedSet
Finset.isWF_bUnion : ∀ {ι : Type u_1} {α : Type u_2} [inst : Preorder α] (s : Finset ι) {f : ι → Set α},
  (⋃ i ∈ s, f i).IsWF ↔ ∀ i ∈ s, (f i).IsWF
-- Init.GrindInstances.Ring.Fin
Lean.Grind.Fin.mul_comm : ∀ {n : ℕ} (a b : Fin n), a * b = b * a
-- Mathlib.Data.List.Basic
List.mem_pure : ∀ {α : Type u} (x y : α), x ∈ pure y ↔ x = y
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.mkIdTerminal_from_left : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} (Y : CategoryTheory.Over X),
  CategoryTheory.Over.Hom.left (CategoryTheory.Over.mkIdTerminal.from Y) = Y.hom
-- Mathlib.RingTheory.Congruence.Defs
/-- The map sending a ring congruence relation to its underlying equivalence
relation is injective.  -/
RingCon.ext'' : ∀ {R : Type u_1} [inst : Add R] [inst_1 : Mul R] {c d : RingCon R}, c.toSetoid = d.toSetoid → c = d
-- Lean.Meta.Tactic.SplitIf
_private.Lean.Meta.Tactic.SplitIf.0.Lean.Meta.findSplit?.find? : Lean.Meta.SplitKind → Lean.ExprSet → Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.rightHomologyιNatTrans_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasKernels C] [inst_3 : CategoryTheory.Limits.HasCokernels C]
  (S : CategoryTheory.ShortComplex C), (CategoryTheory.ShortComplex.rightHomologyιNatTrans C).app S = S.rightHomologyι
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.div_eq_one' : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {r : R} (hr : r ∈ S),
  r /ₒ ⟨r, hr⟩ = 1
-- Mathlib.Topology.UniformSpace.LocallyUniformConvergence
TendstoLocallyUniformlyOn.union : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {F : ι → α → β}
  {f : α → β} {s s' : Set α} {p : Filter ι},
  IsOpen s →
    IsOpen s' →
      TendstoLocallyUniformlyOn F f p s → TendstoLocallyUniformlyOn F f p s' → TendstoLocallyUniformlyOn F f p (s ∪ s')
-- Lean.Environment
Lean.EnvExtension.AsyncMode.async.injEq : ∀ (branch branch_1 : Lean.AsyncBranch),
  (Lean.EnvExtension.AsyncMode.async branch = Lean.EnvExtension.AsyncMode.async branch_1) = (branch = branch_1)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_insert : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α] (h : t.WF) {k a : α} {v : β k},
  (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.getKey! a = if compare k a = Ordering.eq then k else t.getKey! a
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip.0.Std.IterM.step_intermediateZip.match_1.eq_1 : ∀ {α₁ β₁ : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α₁ m β₁] {it₁ : Std.IterM m β₁}
  (motive : it₁.Step → Sort u_3) (it₁' : Std.IterM m β₁) (out : β₁)
  (hp : it₁.IsPlausibleStep (Std.IterStep.yield it₁' out))
  (h_1 :
    (it₁' : Std.IterM m β₁) →
      (out : β₁) → (hp : it₁.IsPlausibleStep (Std.IterStep.yield it₁' out)) → motive ⟨Std.IterStep.yield it₁' out, hp⟩)
  (h_2 :
    (it₁' : Std.IterM m β₁) → (hp : it₁.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', hp⟩)
  (h_3 : (hp : it₁.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, hp⟩),
  (match ⟨Std.IterStep.yield it₁' out, hp⟩ with
    | ⟨Std.IterStep.yield it₁' out, hp⟩ => h_1 it₁' out hp
    | ⟨Std.IterStep.skip it₁', hp⟩ => h_2 it₁' hp
    | ⟨Std.IterStep.done, hp⟩ => h_3 hp) =
    h_1 it₁' out hp
-- Init.Data.Iterators.Lemmas.Combinators.ULift
Std.Iter.count_uLift : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {it : Std.Iter β} [Std.Iterators.Finite α Id]
  [inst_2 : Std.IteratorLoop α Id Id] [Std.LawfulIteratorLoop α Id Id], it.uLift.length = it.length
-- Aesop.Search.Queue
Aesop.FIFOQueue.mk.inj : ∀ {goals : Array Aesop.GoalRef} {pos : ℕ} {goals_1 : Array Aesop.GoalRef} {pos_1 : ℕ},
  { goals := goals, pos := pos } = { goals := goals_1, pos := pos_1 } → goals = goals_1 ∧ pos = pos_1
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.trans_apply : ∀ {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {E : Type u_5} {E₂ : Type u_6} {E₃ : Type u_7} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {σ₁₃ : R →+* R₃} {σ₃₁ : R₃ →+* R}
  {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} [inst_3 : RingHomInvPair σ₁₂ σ₂₁] [inst_4 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_5 : RingHomInvPair σ₁₃ σ₃₁] [inst_6 : RingHomInvPair σ₃₁ σ₁₃] [inst_7 : RingHomInvPair σ₂₃ σ₃₂]
  [inst_8 : RingHomInvPair σ₃₂ σ₂₃] [inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_10 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁]
  [inst_11 : SeminormedAddCommGroup E] [inst_12 : SeminormedAddCommGroup E₂] [inst_13 : SeminormedAddCommGroup E₃]
  [inst_14 : Module R E] [inst_15 : Module R₂ E₂] [inst_16 : Module R₃ E₃] (e₁ : E ≃ₛₗᵢ[σ₁₂] E₂) (e₂ : E₂ ≃ₛₗᵢ[σ₂₃] E₃)
  (c : E), (e₁.trans e₂) c = e₂ (e₁ c)
-- Mathlib.Topology.Compactness.Compact
/-- A compact discrete space is finite.  -/
finite_of_compact_of_discrete : ∀ {X : Type u} [inst : TopologicalSpace X] [CompactSpace X] [DiscreteTopology X], Finite X
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.StructuralAtom.rightUnitor.sizeOf_spec : ∀ (e : Lean.Expr) (f : Mathlib.Tactic.BicategoryLike.Mor₁),
  sizeOf (Mathlib.Tactic.BicategoryLike.StructuralAtom.rightUnitor e f) = 1 + sizeOf e + sizeOf f
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.ext_succ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} {F G : CategoryTheory.ComposableArrows C (n + 1)}
  (h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯) (h : F.δ₀ = G.δ₀),
  F.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 ⋯ =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₀)
        (CategoryTheory.CategoryStruct.comp (G.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 ⋯)
          (CategoryTheory.eqToHom ⋯)) →
    F = G
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Append
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.Append.0.Std.IterM.step_append.match_1.splitter : {α₁ β : Type u_1} →
  {m : Type u_1 → Type u_2} →
    [inst : Std.Iterator α₁ m β] →
      {it₁ : Std.IterM m β} →
        (motive : it₁.Step → Sort u_3) →
          (x : it₁.Step) →
            ((it₁' : Std.IterM m β) →
                (out : β) →
                  (h : it₁.IsPlausibleStep (Std.IterStep.yield it₁' out)) → motive ⟨Std.IterStep.yield it₁' out, h⟩) →
              ((it₁' : Std.IterM m β) →
                  (h : it₁.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', h⟩) →
                ((h : it₁.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩) → motive x
-- Mathlib.MeasureTheory.Integral.MeanInequalities
/-- **Minkowski's inequality for functions** `α → ℝ≥0∞`: the `ℒp` seminorm of the sum of two
functions is bounded by the sum of their `ℒp` seminorms.  -/
ENNReal.lintegral_Lp_add_le : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : ℝ} {f g : α → ENNReal},
  AEMeasurable f μ →
    AEMeasurable g μ →
      1 ≤ p →
        (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤
          (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
-- Mathlib.Analysis.Calculus.Gradient.Basic
HasGradientAt.congr_of_eventuallyEq : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {f' x : F} {f₁ : F → 𝕜},
  HasGradientAt f f' x → f₁ =ᶠ[nhds x] f → HasGradientAt f₁ f' x
-- Mathlib.Combinatorics.Graph.Maps
Graph.map_isLoopAt : ∀ {α : Type u_1} {α' : Type u_2} {β : Type u_4} {G : Graph α β} {e : β} {x : α'} (f : α → α'),
  (Graph.map f G).IsLoopAt e x ↔ ∃ u v, G.IsLink e u v ∧ f u = x ∧ f v = x
-- Mathlib.RingTheory.Congruence.Defs
RingCon.instCommSemigroupQuotient : {R : Type u_1} → [inst : Add R] → [inst_1 : CommSemigroup R] → (c : RingCon R) → CommSemigroup c.Quotient
-- Mathlib.Data.List.Intervals
List.Ico.filter_le_of_le_bot : ∀ {n m l : ℕ}, l ≤ n → List.filter (fun x => decide (l ≤ x)) (List.Ico n m) = List.Ico n m
-- Mathlib.Algebra.Field.Subfield.Basic
/-- An induction principle for closure membership. If `p` holds for `1`, and all elements
of `s`, and is preserved under addition, negation, and multiplication, then `p` holds for all
elements of the closure of `s`.  -/
Subfield.closure_induction : ∀ {K : Type u} [inst : DivisionRing K] {s : Set K} {p : (x : K) → x ∈ Subfield.closure s → Prop},
  (∀ (x : K) (hx : x ∈ s), p x ⋯) →
    p 1 ⋯ →
      (∀ (x y : K) (hx : x ∈ Subfield.closure s) (hy : y ∈ Subfield.closure s), p x hx → p y hy → p (x + y) ⋯) →
        (∀ (x : K) (hx : x ∈ Subfield.closure s), p x hx → p (-x) ⋯) →
          (∀ (x : K) (hx : x ∈ Subfield.closure s), p x hx → p x⁻¹ ⋯) →
            (∀ (x y : K) (hx : x ∈ Subfield.closure s) (hy : y ∈ Subfield.closure s), p x hx → p y hy → p (x * y) ⋯) →
              ∀ {x : K} (h : x ∈ Subfield.closure s), p x h