mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Internal.Order.Basic
_private.Init.Internal.Order.Basic.0.EST.bind.match_1.eq_1 : ∀ {ε σ α : Type} (motive : EST.Out ε σ α → Sort u_1) (a : α) (s : Void σ)
  (h_1 : (a : α) → (s : Void σ) → motive (EST.Out.ok a s)) (h_2 : (e : ε) → (s : Void σ) → motive (EST.Out.error e s)),
  (match EST.Out.ok a s with
    | EST.Out.ok a s => h_1 a s
    | EST.Out.error e s => h_2 e s) =
    h_1 a s
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.size_diff_eq_size_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  (∀ a ∈ t₁, a ∉ t₂) → (t₁ \ t₂).size = t₁.size
-- Mathlib.RingTheory.Coprime.Lemmas
IsRelPrime.pow_right : ∀ {α : Type u_1} [inst : CommMonoid α] [DecompositionMonoid α] {x y : α} {n : ℕ}, IsRelPrime x y → IsRelPrime x (y ^ n)
-- Mathlib.GroupTheory.Sylow
Sylow.dvd_card_of_dvd_card : ∀ {G : Type u} [inst : Group G] [Finite G] {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G),
  p ∣ Nat.card G → p ∣ Nat.card ↥↑P
-- Mathlib.Control.Traversable.Equiv
Equiv.lawfulFunctor' : ∀ {t t' : Type u → Type u} (eqv : (α : Type u) → t α ≃ t' α) [inst : Functor t] [LawfulFunctor t] [F : Functor t'],
  (∀ {α β : Type u} (f : α → β), Functor.map f = Equiv.map eqv f) →
    (∀ {α β : Type u} (f : β), Functor.mapConst f = (Equiv.map eqv ∘ Function.const α) f) → LawfulFunctor t'
-- Mathlib.LinearAlgebra.Finsupp.Pi
/-- If `α` has a unique term, then the type of finitely supported functions `α →₀ M` is
`R`-linearly equivalent to `M`.  -/
Finsupp.LinearEquiv.finsuppUnique : (R : Type u_1) →
  (M : Type u_4) →
    [inst : AddCommMonoid M] →
      [inst_1 : Semiring R] → [inst_2 : Module R M] → (α : Type u_5) → [Unique α] → (α →₀ M) ≃ₗ[R] M
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_mono_on : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E] {μ : MeasureTheory.Measure X} {f g : X → E}
  {s : Set X} [ClosedIciTopology E],
  MeasureTheory.IntegrableOn f s μ →
    MeasureTheory.IntegrableOn g s μ →
      MeasurableSet s → (∀ x ∈ s, f x ≤ g x) → ∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in s, g x ∂μ
-- Init.Data.List.Lemmas
List.map_flatten : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {L : List (List α)},
  List.map f L.flatten = (List.map (List.map f) L).flatten
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.image2_sub : ∀ {α : Type u_2} [inst : Sub α] {s t : Set α}, Set.image2 (fun x1 x2 => x1 - x2) s t = s - t
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.dist_comm : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V}, G.dist u v = G.dist v u
-- Mathlib.MeasureTheory.VectorMeasure.WithDensityVec
_private.Mathlib.MeasureTheory.VectorMeasure.WithDensityVec.0.MeasureTheory.VectorMeasure.«term_→ₛ_» : Lean.TrailingParserDescr
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKeyD_filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp}
  [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Option (γ a)} {k fallback : α}
  (h : t.WF),
  (Std.DTreeMap.Raw.filterMap f t).getKeyD k fallback =
    ((t.getKey? k).pfilter fun x h' => (f x (t.get x ⋯)).isSome).getD fallback
-- Mathlib.Order.Birkhoff
OrderEmbedding.coe_birkhoffFinset : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : Fintype α] [inst_2 : DecidablePred SupIrred] (a : α),
  ↑(OrderEmbedding.birkhoffFinset a) = OrderEmbedding.birkhoffSet a
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.sqrt_nonneg : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalRing A] [inst_2 : TopologicalSpace A] [inst_3 : StarRing A]
  [inst_4 : Module ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : StarOrderedRing A]
  [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A] (a : A),
  0 ≤ CFC.sqrt a
-- Init.Control.Lawful.MonadAttach.Instances
_private.Init.Control.Lawful.MonadAttach.Instances.0.EStateM.bind.match_1.eq_1 : ∀ {ε σ α : Type u_1} (motive : EStateM.Result ε σ α → Sort u_2) (a : α) (s : σ)
  (h_1 : (a : α) → (s : σ) → motive (EStateM.Result.ok a s))
  (h_2 : (e : ε) → (s : σ) → motive (EStateM.Result.error e s)),
  (match EStateM.Result.ok a s with
    | EStateM.Result.ok a s => h_1 a s
    | EStateM.Result.error e s => h_2 e s) =
    h_1 a s
-- Batteries.Control.LawfulMonadState
LawfulMonadStateOf.instStateRefT'OfLawfulMonad : ∀ {m : Type → Type} {ω σ : Type} [inst : Monad m] [LawfulMonad m] [inst_2 : MonadStateOf σ m] [LawfulMonadStateOf σ m],
  LawfulMonadStateOf σ (StateRefT' ω σ m)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
Complex.hasSum_sin' : ∀ (z : ℂ), HasSum (fun n => (z * Complex.I) ^ (2 * n + 1) / ↑(2 * n + 1).factorial / Complex.I) (Complex.sin z)
-- Mathlib.MeasureTheory.Constructions.Cylinders
MeasureTheory.measurable_cylinderEvent_apply : ∀ {ι : Type u_2} {X : ι → Type u_3} [m : (i : ι) → MeasurableSpace (X i)] {Δ : Set ι} {i : ι},
  i ∈ Δ → Measurable fun f => f i
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.mem_powerset : ∀ {x y : ZFSet.{u}}, y ∈ x.powerset ↔ y ⊆ x
-- Mathlib.Data.ENNReal.Inv
ENNReal.mul_inv_cancel : ∀ {a : ENNReal}, a ≠ 0 → a ≠ ⊤ → a * a⁻¹ = 1
-- Mathlib.Order.InitialSeg
InitialSeg.acc : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : InitialSeg r s) (a : α),
  Acc r a ↔ Acc s (f a)
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
/-- Binary **rearrangement inequality**.  -/
mul_add_mul_lt_mul_add_mul' : ∀ {R : Type u} [inst : Semiring R] [inst_1 : PartialOrder R] {a b c d : R} [AddLeftReflectLT R] [ExistsAddOfLE R]
  [MulPosStrictMono R] [AddLeftStrictMono R], b < a → d < c → a * d + b * c < a * c + b * d
-- Lean.Meta.Tactic.SolveByElim
/-- Create or modify a `Config` which
calls `synthInstance` on any goal for which no lemma applies.  -/
Lean.Meta.SolveByElim.SolveByElimConfig.synthInstanceAfter : optParam Lean.Meta.SolveByElim.SolveByElimConfig { } → Lean.Meta.SolveByElim.SolveByElimConfig
-- Mathlib.Algebra.Opposites
AddOpposite.op_inv : ∀ {α : Type u_1} [inst : Inv α] (a : α), AddOpposite.op a⁻¹ = (AddOpposite.op a)⁻¹
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.contains_union : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  (t₁ ∪ t₂).contains k = (t₁.contains k || t₂.contains k)
-- Mathlib.Data.Finsupp.NeLocus
Finsupp.neLocus_add_left : ∀ {α : Type u_1} {N : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq N] [inst_2 : AddLeftCancelMonoid N]
  (f g h : α →₀ N), (f + g).neLocus (f + h) = g.neLocus h
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
NonUnitalSubsemiring.coe_zero : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] (s : NonUnitalSubsemiring R), ↑0 = 0
-- Mathlib.Order.SupIndep
iSupIndep.sSupIndep_range : ∀ {α : Type u_1} {ι : Type u_3} [inst : CompleteLattice α] {t : ι → α}, iSupIndep t → sSupIndep (Set.range t)
-- Std.Do.WP.SimpLemmas
Std.Do.WP.ReaderT_run : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {ρ α : Type u} {r : ρ} {Q : Std.Do.PostCond α ps}
  [inst : Std.Do.WP m ps] (x : ReaderT ρ m α),
  (Std.Do.wp (x.run r)).apply Q = (Std.Do.wp x).apply (fun a x => Q.1 a, Q.2) r
-- Mathlib.RingTheory.Localization.Module
LinearMap.extendScalarsOfIsLocalization_apply' : ∀ {R : Type u_3} [inst : CommSemiring R] (S : Submonoid R) (A : Type u_4) [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] [inst_3 : IsLocalization S A] {M : Type u_5} {N : Type u_6} [inst_4 : AddCommMonoid M]
  [inst_5 : Module R M] [inst_6 : Module A M] [inst_7 : IsScalarTower R A M] [inst_8 : AddCommMonoid N]
  [inst_9 : Module R N] [inst_10 : Module A N] [inst_11 : IsScalarTower R A N] (f : M →ₗ[R] N) (x : M),
  (LinearMap.extendScalarsOfIsLocalization S A f) x = f x
-- Mathlib.Analysis.Asymptotics.LinearGrowth
/-- Upper linear growth as a `SupBotHom`.  -/
LinearGrowth.linearGrowthSupBotHom : SupBotHom (ℕ → EReal) EReal
-- Mathlib.Order.Filter.Finite
/-- **Alias** of `Filter.eventually_all_finite`. -/
Set.Finite.eventually_all : ∀ {α : Type u} {ι : Type u_2} {I : Set ι},
  I.Finite → ∀ {l : Filter α} {p : ι → α → Prop}, (∀ᶠ (x : α) in l, ∀ i ∈ I, p i x) ↔ ∀ i ∈ I, ∀ᶠ (x : α) in l, p i x
-- Mathlib.Algebra.Module.Presentation.Basic
/-- Constructor for `Module.Presentation`.  -/
Module.Presentation.ofIsPresentation : {A : Type u} →
  [inst : Ring A] →
    {M : Type v} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module A M] →
          {relations : Module.Relations A} →
            {solution : relations.Solution M} → solution.IsPresentation → Module.Presentation A M
-- Lean.Expr
Lean.Int.mkInstAdd : Lean.Expr
-- Mathlib.FieldTheory.SeparableClosure
IntermediateField.insepDegree_top : ∀ {F : Type u} (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type w) [inst_3 : Field K]
  [inst_4 : Algebra F K] [inst_5 : Algebra E K] [inst_6 : IsScalarTower F E K],
  Field.insepDegree F ↥⊤ = Field.insepDegree F K
-- Init.Data.Nat.Basic
Nat.add_sub_self_left : ∀ (a b : ℕ), a + b - a = b
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.nonUnitalNonAssocRing : {α : Type u} → [Mul α] → NonUnitalNonAssocRing (FreeAbelianGroup α)
-- Init.Data.Int.DivMod.Lemmas
Int.bmod_eq_emod : ∀ (x : ℤ) (m : ℕ), x.bmod m = x % ↑m - ↑(if x % ↑m ≥ (↑m + 1) / 2 then m else 0)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse_obj_right_hom : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T)
  (G : CategoryTheory.Functor D T) (c : C) (Y : CategoryTheory.Comma ((CategoryTheory.Under.forget c).comp F) G),
  ((CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse F G c).obj Y).right.hom = Y.hom
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
SSet.Truncated.Edge.CompStruct.mk : {X : SSet.Truncated 2} →
  {x₀ x₁ x₂ : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge._proof_1 })} →
    {e₀₁ : SSet.Truncated.Edge x₀ x₁} →
      {e₁₂ : SSet.Truncated.Edge x₁ x₂} →
        {e₀₂ : SSet.Truncated.Edge x₀ x₂} →
          (simplex : X.obj (Opposite.op { obj := { len := 2 }, property := SSet.Truncated.Edge.CompStruct._proof_1 })) →
            autoParam
                ((CategoryTheory.ConcreteCategory.hom
                      (X.map
                        (SimplexCategory.Truncated.δ₂ 2 SSet.Truncated.Edge._proof_2
                            SSet.Truncated.Edge.CompStruct._proof_2).op))
                    simplex =
                  e₀₁.edge)
                SSet.Truncated.Edge.CompStruct.d₂._autoParam →
              autoParam
                  ((CategoryTheory.ConcreteCategory.hom
                        (X.map
                          (SimplexCategory.Truncated.δ₂ 0 SSet.Truncated.Edge._proof_2
                              SSet.Truncated.Edge.CompStruct._proof_2).op))
                      simplex =
                    e₁₂.edge)
                  SSet.Truncated.Edge.CompStruct.d₀._autoParam →
                autoParam
                    ((CategoryTheory.ConcreteCategory.hom
                          (X.map
                            (SimplexCategory.Truncated.δ₂ 1 SSet.Truncated.Edge._proof_2
                                SSet.Truncated.Edge.CompStruct._proof_2).op))
                        simplex =
                      e₀₂.edge)
                    SSet.Truncated.Edge.CompStruct.d₁._autoParam →
                  e₀₁.CompStruct e₁₂ e₀₂
-- Mathlib.Topology.Order.LeftRightNhds
nhdsGT_eq_bot_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {a : α},
  nhdsWithin a (Set.Ioi a) = ⊥ ↔ IsTop a ∨ ∃ b, a ⋖ b
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the forward direction of `le_sub_iff_add_le`. -/
add_le_of_le_sub_right : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddRightMono α] {a b c : α}, a ≤ c - b → a + b ≤ c
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.comp_apply : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Min α] [inst_1 : Top α] [inst_2 : Min β] [inst_3 : Top β]
  [inst_4 : Min γ] [inst_5 : Top γ] (f : InfTopHom β γ) (g : InfTopHom α β) (a : α), (f.comp g) a = f (g a)
-- Mathlib.AlgebraicGeometry.Geometrically.Integral
AlgebraicGeometry.GeometricallyIntegral.iff_geometricallyIntegral_fiber : ∀ {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S),
  AlgebraicGeometry.GeometricallyIntegral f ↔
    ∀ (s : ↥S), AlgebraicGeometry.GeometricallyIntegral (AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField f s)
-- Mathlib.Order.CompleteLattice.Defs
sSup_eq_top : ∀ {α : Type u_1} [inst : CompleteLinearOrder α] {s : Set α}, sSup s = ⊤ ↔ ∀ b < ⊤, ∃ a ∈ s, b < a
-- Mathlib.Topology.WithTopology
WithTopology.instLattice : {X : Type u_1} → (t : TopologicalSpace X) → [Lattice X] → Lattice (WithTopology X t)
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.instHasDistribNegSubtypeGeneralLinearGroupMemSubgroupGLPos : {n : Type u} →
  {R : Type v} →
    [inst : DecidableEq n] →
      [inst_1 : Fintype n] →
        [inst_2 : CommRing R] →
          [inst_3 : LinearOrder R] →
            [inst_4 : IsStrictOrderedRing R] → [Fact (Even (Fintype.card n))] → HasDistribNeg ↥(Matrix.GLPos n R)
-- Mathlib.GroupTheory.Coxeter.Inversion
/-- `t : W` is a *reflection* of the Coxeter system `cs` if it is of the form
$w s_i w^{-1}$, where $w \in W$ and $s_i$ is a simple reflection.  -/
CoxeterSystem.IsReflection : {B : Type u_1} → {W : Type u_2} → [inst : Group W] → {M : CoxeterMatrix B} → CoxeterSystem M W → W → Prop
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.CoreMonoidal.μIso_hom_natural_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} (self : F.CoreMonoidal) {X Y : C} (X' : C) (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f))
      (self.μIso X' Y).hom =
    CategoryTheory.CategoryStruct.comp (self.μIso X' X).hom
      (F.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X' f))
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.CommRing.mk.sizeOf_spec : ∀ (toRing : Lean.Meta.Grind.Arith.CommRing.Ring) (invFn? : Option Lean.Expr) (semiringId? : Option ℕ)
  (commSemiringInst commRingInst : Lean.Expr) (noZeroDivInst? fieldInst? : Option Lean.Expr)
  (powIdentityInst? : Option (Lean.Expr × Lean.Expr × ℕ))
  (denoteEntries : Lean.PArray (Lean.Expr × Lean.Meta.Grind.Arith.CommRing.RingExpr)) (nextId steps : ℕ)
  (queue : Lean.Meta.Grind.Arith.CommRing.Queue) (basis : List Lean.Meta.Grind.Arith.CommRing.EqCnstr)
  (diseqs : Lean.PArray Lean.Meta.Grind.Arith.CommRing.DiseqCnstr) (recheck : Bool) (invSet : Lean.PHashSet Lean.Expr)
  (powIdentityVarCount : ℕ) (numEq0? : Option Lean.Meta.Grind.Arith.CommRing.EqCnstr) (numEq0Updated : Bool),
  sizeOf
      { toRing := toRing, invFn? := invFn?, semiringId? := semiringId?, commSemiringInst := commSemiringInst,
        commRingInst := commRingInst, noZeroDivInst? := noZeroDivInst?, fieldInst? := fieldInst?,
        powIdentityInst? := powIdentityInst?, denoteEntries := denoteEntries, nextId := nextId, steps := steps,
        queue := queue, basis := basis, diseqs := diseqs, recheck := recheck, invSet := invSet,
        powIdentityVarCount := powIdentityVarCount, numEq0? := numEq0?, numEq0Updated := numEq0Updated } =
    1 + sizeOf toRing + sizeOf invFn? + sizeOf semiringId? + sizeOf commSemiringInst + sizeOf commRingInst +
                                sizeOf noZeroDivInst? +
                              sizeOf fieldInst? +
                            sizeOf powIdentityInst? +
                          sizeOf denoteEntries +
                        sizeOf nextId +
                      sizeOf steps +
                    sizeOf queue +
                  sizeOf basis +
                sizeOf diseqs +
              sizeOf recheck +
            sizeOf invSet +
          sizeOf powIdentityVarCount +
        sizeOf numEq0? +
      sizeOf numEq0Updated
-- Init.Data.Vector.Attach
Vector.mem_pmap_of_mem : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {p : α → Prop} {f : (a : α) → p a → β} {xs : Vector α n} {H : ∀ a ∈ xs, p a}
  {a : α} (h : a ∈ xs), f a ⋯ ∈ Vector.pmap f xs H
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_fst : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g]
  (i j : 𝒰.I₀),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV 𝒰 f g i j)
      (CategoryTheory.Limits.pullback.fst
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f j) f) g) (𝒰.f j))
        (𝒰.f i)) =
    CategoryTheory.Limits.pullback.snd
      (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) (𝒰.f i))
      ((AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).ι j)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.size_left_le_size_union : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp],
  t₁.size ≤ (t₁ ∪ t₂).size
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.le_liminf_mul : ∀ {α : Type u_3} {f : Filter α} {u v : α → EReal},
  0 ≤ᶠ[f] u → 0 ≤ᶠ[f] v → Filter.liminf u f * Filter.liminf v f ≤ Filter.liminf (u * v) f
-- Mathlib.Data.List.Defs
/-- `iterateTR.loop f a n l := iterate f a n ++ reverse l`.  -/
List.iterateTR.loop : {α : Type u_1} → (α → α) → α → ℕ → List α → List α
-- Mathlib.Algebra.Homology.Embedding.HomEquiv
ComplexShape.Embedding.homEquiv_apply_coe : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c') (L : HomologicalComplex C c)
  [inst_3 : e.IsRelIff] (ψ : K ⟶ L.extend e), ↑((e.homEquiv K L) ψ) = e.homRestrict ψ
-- Mathlib.FieldTheory.PrimitiveElement
Field.primitive_element_iff_minpoly_degree_eq : ∀ (F : Type u_3) {E : Type u_4} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [FiniteDimensional F E]
  (α : E), F⟮α⟯ = ⊤ ↔ (minpoly F α).degree = ↑(Module.finrank F E)
-- Std.Do.WP.SimpLemmas
Std.Do.WP.control_MonadControlT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {n : Type u → Type u_1} {α : Type u} {Q : Std.Do.PostCond α ps}
  [inst : Bind n] [inst_1 : Std.Do.WP n ps] [inst_2 : MonadControlT m n]
  (f : ({β : Type u} → n β → m (stM m n β)) → m (stM m n α)),
  (Std.Do.wp (control f)).apply Q = (Std.Do.wp (liftWith f >>= restoreM)).apply Q
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.coe_toAddMonoidHom : ∀ {M : Type u_4} {N : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (e : M ≃+ N), ⇑e.toAddMonoidHom = ⇑e
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
CochainComplex.mappingCone.trianglehMapOfHomotopy_hom₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {K₁ L₁ K₂ L₂ : CochainComplex C ℤ} {φ₁ : K₁ ⟶ L₁}
  {φ₂ : K₂ ⟶ L₂} {a : K₁ ⟶ K₂} {b : L₁ ⟶ L₂}
  (H : Homotopy (CategoryTheory.CategoryStruct.comp φ₁ b) (CategoryTheory.CategoryStruct.comp a φ₂)),
  (CochainComplex.mappingCone.trianglehMapOfHomotopy H).hom₁ = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map a
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
/-- The induced map on finite quotients coming from a morphism to `P`.  -/
ProfiniteAddGrp.ProfiniteCompletion.quotientMap : {G : AddGrpCat} →
  {P : ProfiniteAddGrp.{u}} →
    (f : G ⟶ AddGrpCat.of ↑P.toProfinite.toTop) →
      (H : OpenNormalAddSubgroup ↑P.toProfinite.toTop) →
        FiniteAddGrp.of (↑G ⧸ (ProfiniteAddGrp.ProfiniteCompletion.preimage f H).toAddSubgroup) ⟶
          FiniteAddGrp.of (↑P.toProfinite.toTop ⧸ ↑H.toOpenAddSubgroup)
-- Std.Sat.AIG.Basic
Std.Sat.AIG.mk.sizeOf_spec : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] [inst_2 : SizeOf α] (decls : Array (Std.Sat.AIG.Decl α))
  (cache : Std.Sat.AIG.Cache α decls) (hdag : Std.Sat.AIG.IsDAG α decls) (hzero : 0 < decls.size)
  (hconst : decls[0] = Std.Sat.AIG.Decl.false),
  sizeOf { decls := decls, cache := cache, hdag := hdag, hzero := hzero, hconst := hconst } =
    1 + sizeOf decls + sizeOf cache + sizeOf hzero + sizeOf hconst
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKeyD_maxKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t ≠ ∅ → ∀ {fallback : α}, t.getKeyD t.maxKey! fallback = t.maxKey!
-- Mathlib.Data.Set.Order
MonotoneOn.union : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] {f g : β → Set α} {s : Set β},
  MonotoneOn f s → MonotoneOn g s → MonotoneOn (fun x => f x ∪ g x) s
-- Mathlib.Data.EReal.Operations
/-- For any extended real number `x`, the sum of `⊤` and `x` is equal to `⊤`
if and only if `x` is not `⊥`.  -/
EReal.top_add_iff_ne_bot : ∀ {x : EReal}, ⊤ + x = ⊤ ↔ x ≠ ⊥
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.updateRow.congr_simp : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {inst : DecidableEq m} [inst_1 : DecidableEq m] (M M_1 : Matrix m n α),
  M = M_1 →
    ∀ (i i_1 : m),
      i = i_1 →
        ∀ (b b_1 : n → α),
          b = b_1 →
            ∀ (a a_1 : m), a = a_1 → ∀ (a_2 a_3 : n), a_2 = a_3 → M.updateRow i b a a_2 = M_1.updateRow i_1 b_1 a_1 a_3
-- Mathlib.Analysis.Convex.Intrinsic
/-- Naturality of intrinsic closure under a map whose induced map on affine spans is a
homeomorphism. It is introduced here to share the proof of the affine equivalence and affine
isometry versions below.  -/
_private.Mathlib.Analysis.Convex.Intrinsic.0.intrinsicClosure_image_of_homeomorph_affineSpan : ∀ {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} {Q : Type u_4} {P : Type u_5} [inst : Ring 𝕜] [inst_1 : AddCommGroup V]
  [inst_2 : Module 𝕜 V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module 𝕜 W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q] {f : P → Q} {s : Set P}
  (e : [Nonempty ↑s] → ↥(affineSpan 𝕜 s) → ↥(affineSpan 𝕜 (f '' s))),
  (∀ [inst_9 : Nonempty ↑s], IsHomeomorph e) →
    (∀ [inst_9 : Nonempty ↑s] (x : ↥(affineSpan 𝕜 s)), ↑(e x) = f ↑x) →
      intrinsicClosure 𝕜 (f '' s) = f '' intrinsicClosure 𝕜 s
-- Mathlib.Data.NNRat.Defs
NNRat.num_pos : ∀ {q : ℚ≥0}, 0 < q.num ↔ 0 < q
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.cyclesIsoLeftHomology_hom_inv_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasLeftHomology] (hf : S.f = 0),
  CategoryTheory.CategoryStruct.comp S.leftHomologyπ (S.cyclesIsoLeftHomology hf).inv =
    CategoryTheory.CategoryStruct.id S.cycles
-- Mathlib.Analysis.Convex.Gauge
/-- The gauge evaluated at `0` is always zero (mathematically this requires `0` to be in the set `s`
but, the real infimum of the empty set in Lean being defined as `0`, it holds unconditionally).  -/
gauge_zero : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E}, gauge s 0 = 0