mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.equiv_trans : ∀ {ι' : Type u_2} {M' : Type u_7} [inst : AddCommMonoid M'] {ι : Type u_10} {R : Type u_11} {M : Type u_12}
  [inst_1 : Semiring R] [inst_2 : AddCommMonoid M] [inst_3 : Module R M] (b : Module.Basis ι R M) [inst_4 : Module R M']
  {M'' : Type u_13} (b' : Module.Basis ι' R M') [inst_5 : AddCommMonoid M''] [inst_6 : Module R M''] {ι'' : Type u_14}
  (b'' : Module.Basis ι'' R M'') (e : ι ≃ ι') (e' : ι' ≃ ι''),
  b.equiv b' e ≪≫ₗ b'.equiv b'' e' = b.equiv b'' (e.trans e')
-- Batteries.Data.Vector.Lemmas
Vector.getElem?_succ_scanl : ∀ {β : Type u_1} {α : Type u_2} {n : ℕ} {init : β} {i : ℕ} {f : β → α → β} {as : Vector α n},
  (Vector.scanl f init as)[i + 1]? = (Vector.scanl f init as)[i]?.bind fun x => Option.map (fun y => f x y) as[i]?
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.hasTemperateGrowth : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] (f : SchwartzMap E F), Function.HasTemperateGrowth ⇑f
-- Mathlib.Data.Set.Basic
Set.empty_union : ∀ {α : Type u} (a : Set α), ∅ ∪ a = a
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- Composition by continuous linear equivs on the left respects higher differentiability.  -/
ContinuousLinearEquiv.comp_contDiff_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} {n : WithTop ℕ∞} (e : F ≃L[𝕜] G),
  ContDiff 𝕜 n (⇑e ∘ f) ↔ ContDiff 𝕜 n f
-- Mathlib.Order.DirSupClosed
dirSupInacc_iff_of_linearOrder : ∀ {α : Type u_1} {s : Set α} [inst : LinearOrder α],
  DirSupInacc s ↔ ∀ ⦃d : Set α⦄, d.Nonempty → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → (d ∩ s).Nonempty
-- Mathlib.Data.Finset.SDiff
Finset.sdiff_inter_self : ∀ {α : Type u_1} [inst : DecidableEq α] (s₁ s₂ : Finset α), s₂ \ s₁ ∩ s₁ = ∅
-- Mathlib.NumberTheory.DirichletCharacter.Basic
/-- Primitive character associated to multiplication of Dirichlet characters,
after changing both levels to the same  -/
DirichletCharacter.primitive_mul : {R : Type u_1} →
  [inst : CommMonoidWithZero R] →
    {n m : ℕ} →
      (χ₁ : DirichletCharacter R n) → (χ₂ : DirichletCharacter R m) → DirichletCharacter R (χ₁.mul χ₂).conductor
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.contains_of_contains_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k a : α}, (m.insert k).contains a = true → (k == a) = false → m.contains a = true
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.relativeCellComplexOfMono.Cell.ι_l : ∀ {X Y : SSet} {i : X ⟶ Y} {d : ℕ} (c : SSet.relativeCellComplexOfMono.Cell i d),
  CategoryTheory.CategoryStruct.comp c.ιSigmaBoundary (SSet.relativeCellComplexOfMono.l i d) =
    CategoryTheory.CategoryStruct.comp (SSet.boundary d).ι c.ιSigmaStdSimplex
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.instOne.eq_1 : ∀ (A : Type u_2) (B : Type u_3) [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B],
  ContinuousMonoidHom.instOne A B = { one := { toMonoidHom := 1, continuous_toFun := ⋯ } }
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBMap.size_eq : ∀ {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (t : RBTree.RBMap α β cmp), t.size = t.toList.length
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_predicate_zero : ∀ (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], p 0
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Eta-expanded form of `HasFDerivAt.neg` -/
HasFDerivAt.fun_neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {x : E}, HasFDerivAt f f' x → HasFDerivAt (fun i => -f i) (-f') x
-- Mathlib.Algebra.Lie.Weights.RootSystem
/-- `±α` are the only `K`-multiples of a root `α` that are also (non-zero) roots.  -/
LieAlgebra.IsKilling.eq_neg_or_eq_of_eq_smul : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [inst_4 : LieAlgebra.IsKilling K L] [inst_5 : FiniteDimensional K L] {H : LieSubalgebra K L}
  [inst_6 : H.IsCartanSubalgebra] [inst_7 : LieModule.IsTriangularizable K (↥H) L] (α β : LieModule.Weight K (↥H) L),
  β.IsNonZero → ∀ (k : K), ⇑β = k • ⇑α → β = -α ∨ β = α
-- Mathlib.Analysis.Complex.Norm
Complex.ne_zero_of_re_pos : ∀ {s : ℂ}, 0 < s.re → s ≠ 0
-- Mathlib.CategoryTheory.CatCommSq
CategoryTheory.CatCommSq.hId_iso_inv_app : ∀ {C₁ : Type u_1} {C₃ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} C₃] (L : CategoryTheory.Functor C₁ C₃) (X : C₁),
  (CategoryTheory.CatCommSq.iso (CategoryTheory.Functor.id C₁) L L (CategoryTheory.Functor.id C₃)).inv.app X =
    CategoryTheory.CategoryStruct.id (L.obj X)
-- Mathlib.LinearAlgebra.QuadraticForm.Basis
QuadraticMap.map_finsuppSum' : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticMap R M N) (f : ι →₀ R)
  (g : ι → R → M),
  Q (f.sum g) =
    ∑ p ∈ f.support.sym2, QuadraticMap.polarSym2 (⇑Q) (Sym2.map (fun i => g i (f i)) p) - f.sum fun i a => Q (g i a)
-- Mathlib.CategoryTheory.Limits.Filtered
CategoryTheory.Limits.hasFilteredColimitsOfSize_of_hasColimitsOfSize : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimitsOfSize.{w', w, v, u} C],
  CategoryTheory.Limits.HasFilteredColimitsOfSize.{w', w, v, u} C
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.postcomp_map : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {b c : B} (a : B) (f : b ⟶ c) {X Y : a ⟶ b} (x : X ⟶ Y),
  (CategoryTheory.Bicategory.postcomp a f).map x = CategoryTheory.Bicategory.whiskerRight x f
-- Mathlib.Topology.Order
induced_const : ∀ {α : Type u_1} {β : Type u_2} [t : TopologicalSpace α] {x : α}, TopologicalSpace.induced (fun x_1 => x) t = ⊤
-- Mathlib.Data.Fin.VecNotation
Matrix.vecAlt0_vecAppend : ∀ {α : Type u} {n : ℕ} (v : Fin n → α), Matrix.vecAlt0 ⋯ (Matrix.vecAppend ⋯ v v) = v ∘ fun n_1 => n_1 + n_1
-- Lean.Elab.Tactic.BuiltinTactic
Lean.Elab.Tactic.evalRefl : Lean.Elab.Tactic.Tactic
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.moebius_im : ∀ (g : GL (Fin 2) ℝ) (z : ℂ),
  (UpperHalfPlane.num g z / UpperHalfPlane.denom g z).im =
    ↑(Matrix.GeneralLinearGroup.det g) * z.im / Complex.normSq (UpperHalfPlane.denom g z)
-- Mathlib.Analysis.Polynomial.MahlerMeasure
/-- The Mahler measure of `X - C z` equals `max 1 ‖z‖`.  -/
Polynomial.mahlerMeasure_X_sub_C : ∀ (z : ℂ), (Polynomial.X - Polynomial.C z).mahlerMeasure = max 1 ‖z‖
-- Mathlib.Control.Functor
Functor.Comp.ext : ∀ {F : Type u → Type w} {G : Type v → Type u} {α : Type v} {x y : Functor.Comp F G α}, x.run = y.run → x = y
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get!_diff_of_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} [inst_1 : Inhabited (β k)], k ∈ t₂ → (t₁ \ t₂).get! k = default
-- Mathlib.CategoryTheory.GradedObject.Bifunctor
CategoryTheory.GradedObject.mapBifunctor_obj_obj : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [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₃]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) (I : Type u_4) (J : Type u_5)
  (X : CategoryTheory.GradedObject I C₁) (Y : CategoryTheory.GradedObject J C₂) (ij : I × J),
  ((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).obj Y ij = (F.obj (X ij.1)).obj (Y ij.2)
-- Mathlib.Order.Filter.AtTopBot.BigOperators
/-- **Alias** of `Function.Injective.map_atTop_finsetProd_eq`.

---

Let `g : γ → β` be an injective function and `f : β → α` be a function from the codomain of `g`
to a commutative monoid. Suppose that `f x = 1` outside of the range of `g`. Then the filters
`atTop.map (fun s ↦ ∏ i ∈ s, f (g i))` and `atTop.map (fun s ↦ ∏ i ∈ s, f i)` coincide.

The additive version of this lemma is used to prove the equality `∑' x, f (g x) = ∑' y, f y` under
the same assumptions.  -/
Function.Injective.map_atTop_finset_prod_eq : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_3} [inst : CommMonoid M] {g : α → β},
  Function.Injective g →
    ∀ {f : β → M},
      (∀ x ∉ Set.range g, f x = 1) →
        Filter.map (fun s => ∏ i ∈ s, f (g i)) Filter.atTop = Filter.map (fun s => ∏ i ∈ s, f i) Filter.atTop
-- Lean.MetavarContext
Lean.MetavarContext.MkBindingM.Context.mk.sizeOf_spec : ∀ (quotContext : Lean.Name) (lctx : Lean.LocalContext),
  sizeOf { quotContext := quotContext, lctx := lctx } = 1 + sizeOf quotContext + sizeOf lctx
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_sq_pi_over_two_pow_succ : ∀ (n : ℕ), Real.sin (Real.pi / 2 ^ (n + 2)) ^ 2 = 1 / 2 - Real.sqrtTwoAddSeries 0 n / 4
-- Mathlib.Data.Seq.Computation
/-- right map of `⊕`  -/
Computation.rmap : {α : Type u} → {β : Type v} → {γ : Type w} → (β → γ) → α ⊕ β → α ⊕ γ
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.prod.lift_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F F₁ F₂ : CategoryTheory.Functor C (Type w)} (τ₁ : F ⟶ F₁)
  (τ₂ : F ⟶ F₂),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.FunctorToTypes.prod.lift τ₁ τ₂)
      CategoryTheory.FunctorToTypes.prod.snd =
    τ₂
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
/-- This is an auxiliary result for `trajContent_tendsto_zero`. Consider `f` a sequence of bounded
measurable functions such that `f n` depends only on the first coordinates up to `a n`.
Assume that when integrating `f n` against `partialTraj (k + 1) (a n)`, one gets a non-increasing
sequence of functions which converges to `l`.
Assume then that there exists `ε` and `y : Π i : Iic k, X i` such that
when integrating `f n` against `partialTraj k (a n) y`, you get something at least
`ε` for all `n`. Then there exists `z` such that this remains true when integrating
`f` against `partialTraj (k + 1) (a n) (update y (k + 1) z)`.  -/
ProbabilityTheory.Kernel.le_lmarginalPartialTraj_succ : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))}
  [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] {f : ℕ → ((n : ℕ) → X n) → ENNReal} {a : ℕ → ℕ},
  (∀ (n : ℕ), DependsOn (f n) ↑(Finset.Iic (a n))) →
    (∀ (n : ℕ), Measurable (f n)) →
      ∀ {bound : ENNReal},
        bound ≠ ⊤ →
          (∀ (n : ℕ) (x : (n : ℕ) → X n), f n x ≤ bound) →
            ∀ {k : ℕ},
              (∀ (x : (n : ℕ) → X n),
                  Antitone fun n => ProbabilityTheory.Kernel.lmarginalPartialTraj κ (k + 1) (a n) (f n) x) →
                ∀ {l : ((n : ℕ) → X n) → ENNReal},
                  (∀ (x : (n : ℕ) → X n),
                      Filter.Tendsto (fun n => ProbabilityTheory.Kernel.lmarginalPartialTraj κ (k + 1) (a n) (f n) x)
                        Filter.atTop (nhds (l x))) →
                    ∀ (ε : ENNReal) (y : (i : ↥(Finset.Iic k)) → X ↑i),
                      (∀ (x : (i : ℕ) → X i) (n : ℕ),
                          ε ≤
                            ProbabilityTheory.Kernel.lmarginalPartialTraj κ k (a n) (f n)
                              (Function.updateFinset x (Finset.Iic k) y)) →
                        ∃ z,
                          ∀ (x : (i : ℕ) → X i) (n : ℕ),
                            ε ≤
                              ProbabilityTheory.Kernel.lmarginalPartialTraj κ (k + 1) (a n) (f n)
                                (Function.update (Function.updateFinset x (Finset.Iic k) y) (k + 1) z)
-- Mathlib.Data.List.Sigma
/-- List of keys from a list of key-value pairs  -/
List.keys : {α : Type u} → {β : α → Type v} → List (Sigma β) → List α
-- Mathlib.RingTheory.PowerSeries.Basic
/-- The coercion from polynomials to power series
as a ring homomorphism.
 -/
Polynomial.coeToPowerSeries.ringHom : {R : Type u_1} → [inst : Semiring R] → Polynomial R →+* PowerSeries R
-- Mathlib.Data.Fintype.Option
univ_option : ∀ (α : Type u_3) [inst : Fintype α], Finset.univ = Finset.insertNone Finset.univ
-- Mathlib.GroupTheory.Perm.ClosureSwap
/-- A transitive permutation group generated by transpositions must be the whole symmetric group  -/
surjective_of_isSwap_of_isPretransitive' : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : DecidableEq α] [Finite α]
  (S : Set G),
  (∀ σ ∈ S, (MulAction.toPermHom G α) σ = 1 ∨ ((MulAction.toPermHom G α) σ).IsSwap) →
    Subgroup.closure S = ⊤ → ∀ [h : MulAction.IsPretransitive G α], Function.Surjective ⇑(MulAction.toPermHom G α)
-- Mathlib.Algebra.Module.ZMod
AddSubgroup.toZModSubmodule_toAddSubgroup : ∀ (n : ℕ) {M : Type u_1} [inst : AddCommGroup M] [inst_1 : Module (ZMod n) M] (S : AddSubgroup M),
  ((AddSubgroup.toZModSubmodule n) S).toAddSubgroup = S
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.isReal_comap_iff : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] (f : k ≃+* K) {w : NumberField.InfinitePlace K},
  (w.comap ↑f).IsReal ↔ w.IsReal
-- Mathlib.LinearAlgebra.TensorProduct.RightExactness
/-- For a surjective `f : N →ₗ[R] P`,
the natural equivalence between `Q ⊗ N ⧸ (image of ker f)` to `Q ⊗ P`  -/
lTensor.equiv : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      {P : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : AddCommGroup N] →
              [inst_3 : AddCommGroup P] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : Module R P] →
                      {f : M →ₗ[R] N} →
                        {g : N →ₗ[R] P} →
                          (Q : Type u_5) →
                            [inst_7 : AddCommGroup Q] →
                              [inst_8 : Module R Q] →
                                Function.Exact ⇑f ⇑g →
                                  Function.Surjective ⇑g →
                                    (TensorProduct R Q N ⧸ (LinearMap.lTensor Q f).range) ≃ₗ[R] TensorProduct R Q P
-- Std.Internal.UV.UDP
Std.Internal.UV.UDP.instNonemptySocket : Nonempty Std.Internal.UV.UDP.Socket
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.isAtomicPattern : Lean.Expr → Bool
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
/-- The image of a `Edge.CompStruct` by a morphism of simplicial sets.  -/
SSet.Edge.CompStruct.map : {X Y : SSet} →
  {x₀ x₁ x₂ : X.obj (Opposite.op { len := 0 })} →
    {e₀₁ : SSet.Edge x₀ x₁} →
      {e₁₂ : SSet.Edge x₁ x₂} →
        {e₀₂ : SSet.Edge x₀ x₂} → e₀₁.CompStruct e₁₂ e₀₂ → (f : X ⟶ Y) → (e₀₁.map f).CompStruct (e₁₂.map f) (e₀₂.map f)
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
/-- A category embeds into its `R`-linear completion.
 -/
CategoryTheory.Free.embedding : (R : Type u_1) →
  [inst : CommRing R] →
    (C : Type u) → [inst_1 : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor C (CategoryTheory.Free R C)
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.IsPeriodicPt.left_of_add : ∀ {α : Type u_1} {f : α → α} {x : α} {m n : ℕ},
  Function.IsPeriodicPt f (n + m) x → Function.IsPeriodicPt f m x → Function.IsPeriodicPt f n x
-- Mathlib.Order.Interval.Set.Basic
Set.Ioc_subset_Ioi_self : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ioc b a ⊆ Set.Ioi b
-- Mathlib.CategoryTheory.Category.Preorder
CategoryTheory.orderDualEquivalence_inverse_map : ∀ (X : Type u) [inst : Preorder X] {X_1 Y : Xᵒᵖ} (f : X_1 ⟶ Y),
  (CategoryTheory.orderDualEquivalence X).inverse.map f = CategoryTheory.homOfLE ⋯
-- Init.Grind.ToInt
Lean.Grind.instDecidableEqIntInterval : DecidableEq Lean.Grind.IntInterval
-- Lean.Elab.Tactic.Monotonicity
/-- Environment extensions for monotonicity lemmas  -/
Lean.Meta.Monotonicity.monotoneExt : Lean.SimpleScopedEnvExtension (Lean.Name × Array Lean.Meta.DiscrTree.Key) (Lean.Meta.DiscrTree Lean.Name)
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.withBotDegree_eq_coe_degree_iff : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] (f : MvPolynomial σ R),
  m.withBotDegree f = ↑(m.degree f) ↔ f ≠ 0
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
AlgebraicGeometry.isIso_pushoutSection_of_iSup_eq : ∀ {X Y S T : AlgebraicGeometry.Scheme} {f : T ⟶ S} {g : Y ⟶ X} {iX : X ⟶ S} {iY : Y ⟶ T}
  (H : CategoryTheory.IsPullback g iY iX f) {US : S.Opens} {UT : T.Opens} {UX : X.Opens}
  (hUST : UT ≤ (TopologicalSpace.Opens.map f.base).obj US) (hUSX : UX ≤ (TopologicalSpace.Opens.map iX.base).obj US)
  {UY : Y.Opens} (hUY : UY = (TopologicalSpace.Opens.map g.base).obj UX ⊓ (TopologicalSpace.Opens.map iY.base).obj UT)
  {ι : Type u} [Finite ι] (VX : ι → X.Opens) (hVU : iSup VX = UX),
  (∀ (i : ι), CategoryTheory.IsIso (AlgebraicGeometry.pushoutSection H hUST ⋯ ⋯)) →
    (∀ (i j : ι), CategoryTheory.Mono (AlgebraicGeometry.pushoutSection H hUST ⋯ ⋯)) →
      (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f US UT hUST)).Flat →
        CategoryTheory.IsIso (AlgebraicGeometry.pushoutSection H hUST hUSX hUY)
-- Init.Data.Int.Gcd
Int.gcd_one : ∀ {a : ℤ}, a.gcd 1 = 1
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.MatchClone.getKeyArgs : Lean.Expr → Bool → Bool → Lean.MetaM (Lean.Meta.LazyDiscrTree.Key × Array Lean.Expr)
-- Mathlib.Data.Set.Lattice
Set.nonempty_sInter : ∀ {α : Type u_1} {c : Set (Set α)}, (⋂₀ c).Nonempty ↔ ∃ a, ∀ b ∈ c, a ∈ b
-- Mathlib.RingTheory.Valuation.Integers
/-- This is the special case of `Valuation.Integers.isUnit_of_one` when the valuation is defined
over a field. Let `v` be a valuation on some field `F` and `O` be its integers. For every element
`x` in `O`, `x` is a unit in `O` if and only if the image of `x` in `F` has valuation 1.
 -/
Valuation.Integers.isUnit_of_one' : ∀ {F : Type u} {Γ₀ : Type v} [inst : Field F] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {v : Valuation F Γ₀}
  {O : Type w} [inst_2 : CommRing O] [inst_3 : Algebra O F],
  v.Integers O → ∀ {x : O}, v ((algebraMap O F) x) = 1 → IsUnit x
-- Init.Data.String.Basic
String.toList_eq_nil_iff : ∀ {b : String}, b.toList = [] ↔ b = ""
-- Mathlib.Analysis.Polynomial.Norm
Polynomial.supNorm_zero : ∀ {A : Type u_1} [inst : SeminormedRing A], Polynomial.supNorm 0 = 0
-- Mathlib.LinearAlgebra.TensorProduct.Finiteness
/-- For any element `x` of `M ⊗[R] N`, there exists a finite subset `{ (m_i, n_i) }`
of `M × N`, such that `x` is equal to the sum of `m_i ⊗ₜ[R] n_i`.  -/
TensorProduct.exists_finset : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (x : TensorProduct R M N),
  ∃ S, x = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapAddGrp.instMonoidal : {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] →
            [inst_4 : CategoryTheory.BraidedCategory C] →
              [inst_5 : CategoryTheory.BraidedCategory D] →
                (F : CategoryTheory.Functor C D) → [inst_6 : F.Braided] → F.mapAddGrp.Monoidal
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.mem_of : ∀ {α : Type u_1} {m n : α}, m ∈ FreeAddMonoid.of n ↔ m = n
-- Mathlib.Data.Finsupp.Basic
Finsupp.mem_range_of_mapDomain_ne_zero : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] {f : α → β} {x : α →₀ M} {b : β},
  (Finsupp.mapDomain f x) b ≠ 0 → b ∈ Set.range f
-- Mathlib.Analysis.LocallyConvex.Bounded
Filter.Tendsto.isVonNBounded_range : ∀ (𝕜 : Type u_1) {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] {f : ℕ → E} {x : E},
  Filter.Tendsto f Filter.atTop (nhds x) → Bornology.IsVonNBounded 𝕜 (Set.range f)
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.toArrowArrowFunctor'_obj_hom_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C),
  (CategoryTheory.Square.toArrowArrowFunctor'.obj sq).hom.left = sq.f₁₃
-- Lean.Meta.Tactic.SplitIf
/-- Simplify the `if-then-else` targeted by the `split` tactic. If `useNewSemantics` is `true`, the flag
`backward.split` is ignored.
 -/
Lean.Meta.simpIfLocalDecl : Lean.MVarId → Lean.FVarId → optParam Bool false → Lean.MetaM Lean.MVarId
-- Mathlib.Data.Set.MemPartition
_private.Mathlib.Data.Set.MemPartition.0.memPartition.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.Data.Finset.NAry
Finset.image₂_inter_left : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s s' : Finset α} {t : Finset β}
  [inst_1 : DecidableEq α],
  Function.Injective2 f → Finset.image₂ f (s ∩ s') t = Finset.image₂ f s t ∩ Finset.image₂ f s' t
-- Mathlib.ModelTheory.Arithmetic.Presburger.Basic
FirstOrder.Language.presburger.instAddTerm : {α : Type u_1} → Add (FirstOrder.Language.presburger.Term α)
-- Mathlib.Order.Filter.Pointwise
Filter.pureAddHom.eq_1 : ∀ {α : Type u_2} [inst : Add α], Filter.pureAddHom = { toFun := pure, map_add' := ⋯ }
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.X_pow_dvd_iff : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {s : σ} {n : ℕ} {φ : MvPowerSeries σ R},
  MvPowerSeries.X s ^ n ∣ φ ↔ ∀ (m : σ →₀ ℕ), m s < n → (MvPowerSeries.coeff m) φ = 0
-- Mathlib.Algebra.Group.Action.Basic
AddAction.bijective : ∀ {α : Type u_5} {β : Type u_6} [inst : AddGroup α] [inst_1 : AddAction α β] (g : α), Function.Bijective fun x => g +ᵥ x
-- Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
/-- The function `x ^ (1 / x)` tends to `1` at `+∞`.  -/
tendsto_rpow_div : Filter.Tendsto (fun x => x ^ (1 / x)) Filter.atTop (nhds 1)
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.vadd_graphOn_univ : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : AddCommGroup β] [inst_2 : FunLike F α β]
  [AddMonoidHomClass F α β] (x : α × β) (f : F),
  x +ᵥ Set.graphOn (⇑f) Set.univ = Set.graphOn (fun a => x.2 - f x.1 + f a) Set.univ
-- Mathlib.Algebra.BigOperators.Finprod
finprod_inv_distrib : ∀ {G : Type u_1} {α : Sort u_4} [inst : DivisionCommMonoid G] (f : α → G), ∏ᶠ (x : α), (f x)⁻¹ = (∏ᶠ (x : α), f x)⁻¹
-- Init.Core
/-- `True` is true, and `True.intro` (or more commonly, `trivial`)
is the proof.  -/
trivial : True
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to0.trAux.eq_5 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (M : Λ → Turing.TM1.Stmt Γ Λ σ) (s : Γ) (x : σ) (l : Γ → σ → Λ),
  Turing.TM1to0.trAux M s (Turing.TM1.Stmt.goto l) x = ((some (M (l s x)), x), Turing.TM0.Stmt.write s)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
/-- The set `1 : Set α` is defined as `{1}` in scope `Pointwise`.  -/
Set.one : {α : Type u_2} → [One α] → One (Set α)
-- Mathlib.Logic.Basic
Prop.forall_iff : ∀ {p : Prop → Prop}, (∀ (h : Prop), p h) ↔ p False ∧ p True
-- Mathlib.Analysis.Convex.Function
concaveOn_id : ∀ {𝕜 : Type u_1} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid β]
  [inst_3 : PartialOrder β] [inst_4 : SMul 𝕜 β] {s : Set β}, Convex 𝕜 s → ConcaveOn 𝕜 s id
-- Mathlib.Tactic.FunProp.Theorems
/-- Constant theorem e.g. `Continuous fun x ↦ y`  -/
Mathlib.Meta.FunProp.LambdaTheoremArgs.const : Mathlib.Meta.FunProp.LambdaTheoremArgs