mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.InfoTree.Types
/-- The name of the elaborator that created this info.  -/
Lean.Elab.ElabInfo.elaborator : Lean.Elab.ElabInfo → Lean.Name
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasDerivAt_deriv_iff : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜}, HasDerivAt f (deriv f x) x ↔ DifferentiableAt 𝕜 f x
-- Init.Data.Iterators.Consumers.Monadic.Collect
Std.IterM.toArray.go : {α β : Type w} → {m : Type w → Type w'} → [Monad m] → [Std.Iterator α m β] → Std.IterM m β → Array β → m (Array β)
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
/-- The additive group morphism from `fixingAddSubgroup` of a union
to the iterated `fixingAddSubgroup`.  -/
SubAddAction.fixingAddSubgroup_union_to_fixingAddSubgroup_of_fixingAddSubgroup : {M : Type u_1} →
  {α : Type u_2} →
    [inst : AddGroup M] →
      [inst_1 : AddAction M α] →
        {s t : Set α} →
          ↥(fixingAddSubgroup M (s ∪ t)) →+ ↥(fixingAddSubgroup (↥(fixingAddSubgroup M s)) (Subtype.val ⁻¹' t))
-- Mathlib.CategoryTheory.FiberedCategory.Fibered
/-- Given a diagram
```
                  a
                  -
                  |
                  v
T --g--> R --f--> S
```
we have an isomorphism `T ×_S a ≅ T ×_R (R ×_S a)`  -/
CategoryTheory.Functor.IsFibered.pullbackPullbackIso : {𝒮 : Type u₁} →
  {𝒳 : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳] →
        {p : CategoryTheory.Functor 𝒳 𝒮} →
          [inst_2 : p.IsFibered] →
            {R S T : 𝒮} →
              {a : 𝒳} →
                (ha : p.obj a = S) →
                  (f : R ⟶ S) →
                    (g : T ⟶ R) →
                      CategoryTheory.Functor.IsPreFibered.pullbackObj ha (CategoryTheory.CategoryStruct.comp g f) ≅
                        CategoryTheory.Functor.IsPreFibered.pullbackObj ⋯ g
-- Init.Data.Rat.Lemmas
Rat.neg_le_neg_iff : ∀ {a b : ℚ}, -a ≤ -b ↔ b ≤ a
-- Mathlib.Algebra.Ring.Parity
Even.neg_one_pow : ∀ {α : Type u_2} [inst : Monoid α] [inst_1 : HasDistribNeg α] {n : ℕ}, Even n → (-1) ^ n = 1
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.num_denom_neg : ∀ {K : Type u} [inst : Field K] (x : RatFunc K), (-x).num * x.denom = -x.num * (-x).denom
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.compl_top : ∀ {α : Type u_1} [inst : LE α], ⊤.compl = ⊤
-- Mathlib.Algebra.Group.Defs
_private.Mathlib.Algebra.Group.Defs.0.npowRec.match_1.splitter : {M : Type u_2} →
  (motive : ℕ → M → Sort u_1) →
    (x : ℕ) → (x_1 : M) → ((x : M) → motive 0 x) → ((n : ℕ) → (a : M) → motive n.succ a) → motive x x_1
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.coercions.types : Lean.Option Bool
-- Mathlib.CategoryTheory.Abelian.Pseudoelements
/-- If two pseudoelements `x` and `y` have the same image under some morphism `f`, then we can form
their "difference" `z`. This pseudoelement has the properties that `f z = 0` and for all
morphisms `g`, if `g y = 0` then `g z = g x`.  -/
CategoryTheory.Abelian.Pseudoelement.sub_of_eq_image : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q)
  (x y : CategoryTheory.Abelian.Pseudoelement P),
  CategoryTheory.Abelian.Pseudoelement.pseudoApply f x = CategoryTheory.Abelian.Pseudoelement.pseudoApply f y →
    ∃ z,
      CategoryTheory.Abelian.Pseudoelement.pseudoApply f z = 0 ∧
        ∀ (R : C) (g : P ⟶ R),
          CategoryTheory.Abelian.Pseudoelement.pseudoApply g y = 0 →
            CategoryTheory.Abelian.Pseudoelement.pseudoApply g z = CategoryTheory.Abelian.Pseudoelement.pseudoApply g x
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
UniformContinuous.div : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] [inst_3 : UniformSpace β]
  {f g : β → α}, UniformContinuous f → UniformContinuous g → UniformContinuous fun x => f x / g x
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosSemidef.diag_nonneg : ∀ {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] {A : Matrix n n R},
  A.PosSemidef → ∀ {i : n}, 0 ≤ A i i
-- Lean.Elab.Do.Basic
/-- The type of the monadic result.  -/
Lean.Elab.Do.DoElemCont.resultType : Lean.Elab.Do.DoElemCont → Lean.Expr
-- Batteries.Classes.Order
/-- `LawfulLTCmp cmp` asserts that `cmp x y = .lt` and `x < y` coincide.  -/
Std.LawfulLTCmp : {α : Type u_1} → [LT α] → (α → α → Ordering) → Prop
-- Mathlib.Topology.Sober
genericPoints.equiv_symm_apply : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : T0Space α] [inst_2 : QuasiSober α]
  (x : ↑(irreducibleComponents α)), genericPoints.equiv.symm x = genericPoints.ofComponent x
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.Compacts.isClosed_inter_nonempty_of_isClosed : ∀ {α : Type u_1} [inst : TopologicalSpace α] {F : Set α}, IsClosed F → IsClosed {K | (↑K ∩ F).Nonempty}
-- Plausible.Shrinkable
Plausible.Unit.shrinkable : Plausible.Shrinkable Unit
-- Mathlib.Probability.Kernel.Composition.CompProd
ProbabilityTheory.Kernel.ae_kernel_lt_top : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {s : Set (β × γ)} {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ]
  {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η] (a : α),
  ((κ.compProd η) a) s ≠ ⊤ → ∀ᵐ (b : β) ∂κ a, (η (a, b)) (Prod.mk b ⁻¹' s) < ⊤
-- Mathlib.Order.Fin.Basic
Fin.instLinearOrder : {n : ℕ} → LinearOrder (Fin n)
-- Init.Data.List.Zip
_private.Init.Data.List.Zip.0.List.getElem?_zipWith.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : Option α → Option β → Sort u_3) (a : α) (b : β)
  (h_1 : (a : α) → (b : β) → motive (some a) (some b)) (h_2 : (x : Option α) → (x_1 : Option β) → motive x x_1),
  (match some a, some b with
    | some a, some b => h_1 a b
    | x, x_1 => h_2 x x_1) =
    h_1 a b
-- Init.Data.Array.Subarray
Std.Slice.Internal.SubarrayData.mk.congr_simp : ∀ {α : Type u} (array array_1 : Array α) (e_array : array = array_1) (start start_1 : ℕ) (e_start : start = start_1)
  (stop stop_1 : ℕ) (e_stop : stop = stop_1) (start_le_stop : start ≤ stop) (stop_le_array_size : stop ≤ array.size),
  { array := array, start := start, stop := stop, start_le_stop := start_le_stop,
      stop_le_array_size := stop_le_array_size } =
    { array := array_1, start := start_1, stop := stop_1, start_le_stop := ⋯, stop_le_array_size := ⋯ }
-- Mathlib.Logic.Function.Basic
Function.leftInverse_surjInv : ∀ {α : Sort u} {β : Sort v} {f : α → β} (hf : Function.Bijective f), Function.LeftInverse (Function.surjInv ⋯) f
-- Std.Http.Server
_private.Std.Http.Server.0.Std.Http.Server.frameCancellation : {α : Type} → Std.Http.Server → optParam Bool false → Std.Async.ContextAsync α → Std.Async.ContextAsync α
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_inter_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k fallback : α}, k ∈ t₂ → (t₁ ∩ t₂).getKeyD k fallback = t₁.getKeyD k fallback
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
/-- Restricting to `affineSpan k (Set.range s.points)` can be reversed by mapping through
`AffineSubspace.subtype`.  -/
Affine.Simplex.restrict_map_subtype : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} (s : Affine.Simplex k P n),
  (s.restrict (affineSpan k (Set.range s.points)) ⋯).map (affineSpan k (Set.range s.points)).subtype ⋯ = s
-- Init.Data.BitVec.Basic
/-- Signed less-than-or-equal-to for bitvectors.

SMT-LIB name: `bvsle`.
 -/
BitVec.sle : {n : ℕ} → BitVec n → BitVec n → Bool
-- Mathlib.Algebra.SkewMonoidAlgebra.Lift
SkewMonoidAlgebra.domCongrAlg_toAlgHom : ∀ (k : Type u_1) {G : Type u_2} {H : Type u_3} (A : Type u_4) [inst : Monoid G] [inst_1 : Monoid H]
  [inst_2 : Semiring A] [inst_3 : CommSemiring k] [inst_4 : Algebra k A] [inst_5 : MulSemiringAction G A]
  [inst_6 : MulSemiringAction H A] [inst_7 : SMulCommClass G k A] [inst_8 : SMulCommClass H k A] {e : G ≃* H}
  (he : ∀ (a : G) (x : A), a • x = e a • x),
  ↑(SkewMonoidAlgebra.domCongrAlg k A he) = SkewMonoidAlgebra.mapDomainAlgHom k A he
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- **Alias** of `add_apply`. -/
AddGroupNorm.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
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.sup_toSubmodule : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N N' : LieSubmodule R L M), ↑(N ⊔ N') = ↑N ⊔ ↑N'
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKey!_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] [inst_1 : Inhabited α],
  t.WF → ∀ {k : α} {f : β k → β k}, (t.modify k f).maxKey! = t.maxKey!
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.BilinForm.nondegenerate_iff : ∀ {R : Type u_1} {M : Type u_5} [inst : CommRing R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (B : LinearMap.BilinForm R M),
  (∀ (x : M), 0 ≤ (B x) x) → LinearMap.IsSymm B → (LinearMap.Nondegenerate B ↔ ∀ (x : M), (B x) x = 0 ↔ x = 0)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
AlgebraicGeometry.Scheme.IdealSheafData.ideal_map_of_isAffineHom : ∀ {X Y : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (f : X ⟶ Y) [inst : AlgebraicGeometry.IsAffineHom f]
  (U : ↑Y.affineOpens),
  (I.map f).ideal U =
    Ideal.comap (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.app f ↑U))
      (I.ideal ⟨(TopologicalSpace.Opens.map f.base).obj ↑U, ⋯⟩)
-- Mathlib.Algebra.MvPolynomial.Basic
/-- The coefficient of the monomial `m` in the multi-variable polynomial `p`.  -/
MvPolynomial.coeff : {R : Type u} → {σ : Type u_1} → [inst : CommSemiring R] → (σ →₀ ℕ) → MvPolynomial σ R → R
-- Lean.Data.SMap
Lean.SMap.numBuckets : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Lean.SMap α β → ℕ
-- Mathlib.Analysis.Normed.Module.Ball.Action
isScalarTower_sphere_sphere_closedBall : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : NormedField 𝕜']
  [inst_2 : SeminormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜' E] {r : ℝ}
  [inst_5 : NormedAlgebra 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' E],
  IsScalarTower ↑(Metric.sphere 0 1) ↑(Metric.sphere 0 1) ↑(Metric.closedBall 0 r)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.filter_eq_empty_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Bool},
  Std.ExtDTreeMap.filter f t = ∅ ↔ ∀ (k : α) (h : k ∈ t), f k (t.get k h) = false
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.instIsUpperSetWithUpperSet : ∀ {α : Type u_1} [inst : Preorder α], Topology.IsUpperSet (Topology.WithUpperSet α)
-- Mathlib.Order.Interval.Set.Basic
/-- If `a ≤ b`, then `(b, +∞) ⊆ (a, +∞)`. In preorders, this is just an implication. If you need
the equivalence in linear orders, use `Ioi_subset_Ioi_iff`.  -/
Set.Ioi_subset_Ioi : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, b ≤ a → Set.Ioi a ⊆ Set.Ioi b
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
PseudoMetricSpace.toUniformSpace.hcongr_2 : ∀ (α α' : Type u),
  α = α' →
    ∀ (self : PseudoMetricSpace α) (self' : PseudoMetricSpace α'),
      self ≍ self' → PseudoMetricSpace.toUniformSpace ≍ PseudoMetricSpace.toUniformSpace
-- Init.Data.List.Sublist
List.sublist_nil : ∀ {α : Type u_1} {l : List α}, l.Sublist [] ↔ l = []
-- Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
alternatingGroup.exponent_kleinFour_of_card_eq_four : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α],
  Nat.card α = 4 → Monoid.exponent ↥(alternatingGroup.kleinFour α) = 2
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.ReflPrefunctor.mk.congr_simp : ∀ {V : Type u₁} [inst : CategoryTheory.ReflQuiver V] {W : Type u₂} [inst_1 : CategoryTheory.ReflQuiver W]
  (toPrefunctor toPrefunctor_1 : V ⥤q W) (e_toPrefunctor : toPrefunctor = toPrefunctor_1)
  (map_id :
    ∀ (X : V), toPrefunctor.map (CategoryTheory.ReflQuiver.id X) = CategoryTheory.ReflQuiver.id (toPrefunctor.obj X)),
  { toPrefunctor := toPrefunctor, map_id := map_id } = { toPrefunctor := toPrefunctor_1, map_id := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
/-- A functor between Cartesian monoidal categories is monoidal iff it preserves finite products.
 -/
CategoryTheory.Functor.Monoidal.nonempty_monoidal_iff_preservesFiniteProducts : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D), Nonempty F.Monoidal ↔ CategoryTheory.Limits.PreservesFiniteProducts F
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleSets.ruleSets : Aesop.Frontend.RuleSets → Array Aesop.RuleSetName
-- Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
HomotopicalAlgebra.LeftHomotopyRel.precomp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {f g : X ⟶ Y} [HomotopicalAlgebra.IsFibrant Y],
  HomotopicalAlgebra.LeftHomotopyRel f g →
    ∀ {Z : C} (i : Z ⟶ X),
      HomotopicalAlgebra.LeftHomotopyRel (CategoryTheory.CategoryStruct.comp i f)
        (CategoryTheory.CategoryStruct.comp i g)
-- Mathlib.RingTheory.FinitePresentation
/-- If `e : A ≃ₐ[R] B` and `A` is finitely presented, then so is `B`.  -/
Algebra.FinitePresentation.equiv : ∀ {R : Type w₁} {A : Type w₂} {B : Type w₃} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [Algebra.FinitePresentation R A] (e : A ≃ₐ[R] B),
  Algebra.FinitePresentation R B
-- Mathlib.CategoryTheory.Abelian.SerreClass.Localization
/-- When `L : C ⥤ D` is a localization functor with respect to a Serre class
in the abelian category `C`, this is the functor `(D ⥤ₑ E) ⥤ C ⥤ₑ E`
obtained by precomposition with `L`.  -/
CategoryTheory.ObjectProperty.SerreClassLocalization.whiskeringLeft : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {D : Type u'} →
        [inst_2 : CategoryTheory.Category.{v', u'} D] →
          (L : CategoryTheory.Functor C D) →
            (P : CategoryTheory.ObjectProperty C) →
              [inst_3 : P.IsSerreClass] →
                (E : Type u'') →
                  [inst_4 : CategoryTheory.Category.{v'', u''} E] →
                    [CategoryTheory.Abelian E] →
                      [L.IsLocalization P.isoModSerre] →
                        [inst_7 : CategoryTheory.Preadditive D] →
                          [L.Additive] → CategoryTheory.Functor (D ⥤ₑ E) (C ⥤ₑ E)
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.decodePi.match_3.eq_2 : ∀ (motive : (n : ℕ) → (f : Fin n → ℕ) → Fin (Fin.prod f) → Sort u_1) (n : ℕ) (f : Fin (n + 1) → ℕ) (x : ℕ)
  (hx : x < Fin.prod f) (h_1 : (x : Fin 0 → ℕ) → (x_1 : Fin (Fin.prod x)) → motive 0 x x_1)
  (h_2 : (n : ℕ) → (f : Fin (n + 1) → ℕ) → (x : ℕ) → (hx : x < Fin.prod f) → motive n.succ f ⟨x, hx⟩),
  (match n.succ, f, ⟨x, hx⟩ with
    | 0, x, x_1 => h_1 x x_1
    | n.succ, f, ⟨x, hx⟩ => h_2 n f x hx) =
    h_2 n f x hx
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.Algebra.instIsScalarTowerCarrier : ∀ {S₀ : Type u₀} [inst : CommSemiring S₀] {S : Type u} [inst_1 : Semiring S] [inst_2 : Algebra S₀ S]
  {M : SemimoduleCat S}, IsScalarTower S₀ S ↑M
-- Init.Sym.Lemmas
Lean.Sym.String.lt_eq_true : ∀ (a b : String), decide (a < b) = true → (a < b) = True
-- Mathlib.FieldTheory.SeparableDegree
/-- If the field extension `E / F` is transcendental, then `Field.finSepDegree F E = 0`, which
actually means that `Field.Emb F E` is infinite (see `Field.infinite_emb_of_transcendental`).  -/
Field.finSepDegree_eq_zero_of_transcendental : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [Algebra.Transcendental F E],
  Field.finSepDegree F E = 0
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.isImage_source_target : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y), e.IsImage e.source e.target
-- Init.Data.SInt.Lemmas
Int16.toNatClampNeg_one : Int16.toNatClampNeg 1 = 1
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
SSet.Subcomplex.Pairing.IsRegular.toIsProper : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} [self : P.IsRegular], P.IsProper
-- Std.Data.DTreeMap.Raw.WF
Std.DTreeMap.Raw.WF.union : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] {t₁ t₂ : Std.DTreeMap.Raw α (fun x => β) cmp},
  t₁.WF → t₂.WF → (t₁ ∪ t₂).WF
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
OpenPartialHomeomorph.continuousWithinAt_writtenInExtend_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} {E' : Type u_5} {M' : Type u_6} {H' : Type u_7}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M] (f : OpenPartialHomeomorph M H)
  {I : ModelWithCorners 𝕜 E H} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  [inst_7 : TopologicalSpace H'] [inst_8 : TopologicalSpace M'] {I' : ModelWithCorners 𝕜 E' H'} {s : Set M}
  {f' : OpenPartialHomeomorph M' H'} {g : M → M'} {y : M},
  y ∈ f.source →
    g y ∈ f'.source →
      Set.MapsTo g s f'.source →
        (ContinuousWithinAt (↑(f'.extend I') ∘ g ∘ ↑(f.extend I).symm) (↑(f.extend I).symm ⁻¹' s ∩ Set.range ↑I)
            (↑(f.extend I) y) ↔
          ContinuousWithinAt g s y)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getThenInsertIfNew?_snd : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF → ∀ {k : α} {v : β k}, (m.getThenInsertIfNew? k v).2 = m.insertIfNew k v
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonDeclarationParams : Lean.ToJson Lean.Lsp.DeclarationParams
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.Cover.gluedCoverT'_fst_fst : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.I₀),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.gluedCoverT' 𝒰 x y z)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.f y) (𝒰.f z))
          (CategoryTheory.Limits.pullback.fst (𝒰.f y) (𝒰.f x)))
        (CategoryTheory.Limits.pullback.fst (𝒰.f y) (𝒰.f z))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y))
        (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f z)))
      (CategoryTheory.Limits.pullback.snd (𝒰.f x) (𝒰.f y))
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
/-- Function sending `w : InfinitePlace L` to `w.embedding` if `w.embedding` lies over
`v.embedding`, otherwise to its conjugate.  -/
_private.Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification.0.NumberField.InfinitePlace.embeddingConjugateIte : {K : Type u_4} →
  {L : Type u_5} →
    [inst : Field K] →
      [inst_1 : Field L] → [Algebra K L] → NumberField.InfinitePlace K → NumberField.InfinitePlace L → L →+* ℂ
-- Init.Data.List.Zip
List.zipWith_eq_append_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l₁' l₂' : List γ} {f : α → β → γ} {l₁ : List α} {l₂ : List β},
  List.zipWith f l₁ l₂ = l₁' ++ l₂' ↔
    ∃ ws xs ys zs,
      ws.length = ys.length ∧ l₁ = ws ++ xs ∧ l₂ = ys ++ zs ∧ l₁' = List.zipWith f ws ys ∧ l₂' = List.zipWith f xs zs
-- Mathlib.CategoryTheory.Square
/-- the top-right morphism  -/
CategoryTheory.Square.Hom.τ₂ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → {sq₁ sq₂ : CategoryTheory.Square C} → sq₁.Hom sq₂ → (sq₁.X₂ ⟶ sq₂.X₂)
-- Mathlib.GroupTheory.OrderOfElement
card_zmultiples_le : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : Fintype G] (a : G) {k : ℕ},
  k ≠ 0 → k • a = 0 → Fintype.card ↥(AddSubgroup.zmultiples a) ≤ k
-- Mathlib.CategoryTheory.Functor.Derived.LeftDerived
CategoryTheory.Functor.isLeftDerivedFunctor_iff_isIso_leftDerivedLift : ∀ {C : Type u_3} {D : Type u_1} {H : Type u_2} [inst : CategoryTheory.Category.{v_1, u_3} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_1} D] [inst_2 : CategoryTheory.Category.{v_5, u_2} H]
  (LF : CategoryTheory.Functor D H) {F : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  (α : L.comp LF ⟶ F) (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  [inst_4 : LF.IsLeftDerivedFunctor α W] (G : CategoryTheory.Functor D H) (β : L.comp G ⟶ F),
  G.IsLeftDerivedFunctor β W ↔ CategoryTheory.IsIso (LF.leftDerivedLift α W G β)
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax
CategoryTheory.Oplax.LaxTrans.whiskerLeft_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G H : CategoryTheory.OplaxFunctor B C} (η : F ⟶ G) {θ ι : G ⟶ H} (Γ : θ ⟶ ι) (a : B),
  (CategoryTheory.Oplax.LaxTrans.whiskerLeft η Γ).as.app a =
    CategoryTheory.Bicategory.whiskerLeft (η.app a) (Γ.as.app a)
-- Mathlib.CategoryTheory.Limits.Types.Limits
CategoryTheory.Limits.Types.limit_ext_iff' : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F' : CategoryTheory.Functor J (Type v))
  (x y : CategoryTheory.Limits.limit F'),
  x = y ↔
    ∀ (j : J),
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π F' j)) x =
        (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π F' j)) y
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.mk_le_mk : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Preorder β] {f g : α → β}
  {hf : ∀ (x : β), MeasurableSet (f ⁻¹' {x})} {hg : ∀ (x : β), MeasurableSet (g ⁻¹' {x})} {hf' : (Set.range f).Finite}
  {hg' : (Set.range g).Finite},
  { toFun := f, measurableSet_fiber' := hf, finite_range' := hf' } ≤
      { toFun := g, measurableSet_fiber' := hg, finite_range' := hg' } ↔
    f ≤ g
-- Mathlib.Data.Rat.Cast.Order
Rat.preimage_cast_uIcc : ∀ {K : Type u_5} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] (p q : ℚ),
  Rat.cast ⁻¹' Set.uIcc ↑p ↑q = Set.uIcc p q
-- Mathlib.Analysis.Analytic.Constructions
AnalyticAt.div_const : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝕝 : Type u_8} [inst_3 : NormedDivisionRing 𝕝] [inst_4 : NormedAlgebra 𝕜 𝕝] {x : E}
  {f : E → 𝕝}, AnalyticAt 𝕜 f x → ∀ {c : 𝕝}, AnalyticAt 𝕜 (fun x => f x / c) x
-- Lean.Server.InfoUtils
Lean.Elab.InfoTree.foldInfoM : {m : Type u_1 → Type u_2} →
  {α : Type u_1} → [Monad m] → (Lean.Elab.ContextInfo → Lean.Elab.Info → α → m α) → α → Lean.Elab.InfoTree → m α
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
CategoryTheory.Monoidal.whiskerRight_fst : ∀ {A B : CategoryTheory.Cat} (f : A ⟶ B) (X : CategoryTheory.Cat),
  (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X).toFunctor.comp (CategoryTheory.Prod.fst ↑B ↑X) =
    (CategoryTheory.Prod.fst ↑A ↑X).comp f.toFunctor
-- Mathlib.Algebra.Category.Grp.FilteredColimits
AddGrpCat.FilteredColimits.colimitAddGroup.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J AddGrpCat),
  AddGrpCat.FilteredColimits.colimitAddGroup F =
    { toAddMonoid := (AddGrpCat.FilteredColimits.G F).str, toNeg := AddGrpCat.FilteredColimits.colimitNeg F,
      sub := SubNegMonoid.sub', zsmul := zsmulRec, sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯,
      zsmul_neg' := ⋯, neg_add_cancel := ⋯ }