mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.map_homothety_hausdorffMeasure : ∀ {𝕜 : Type u_4} {E : Type u_5} {P : Type u_6} [inst : NormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : MeasurableSpace P] [inst_4 : MetricSpace P] [inst_5 : NormedAddTorsor E P]
  [inst_6 : BorelSpace P] {d : ℝ},
  0 ≤ d →
    ∀ (x : P) {c : 𝕜},
      c ≠ 0 →
        MeasureTheory.Measure.map (⇑(AffineMap.homothety x c)) (MeasureTheory.Measure.hausdorffMeasure d) =
          ‖c‖₊⁻¹ ^ d • MeasureTheory.Measure.hausdorffMeasure d
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get!_erase_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β], t.WF → ∀ {k : α}, Std.DTreeMap.Raw.Const.get! (t.erase k) k = default
-- Init.Data.List.Lemmas
List.append_inj_right : ∀ {α : Type u_1} {s₁ t₁ s₂ t₂ : List α}, s₁ ++ t₁ = s₂ ++ t₂ → s₁.length = s₂.length → t₁ = t₂
-- Mathlib.Analysis.InnerProductSpace.Positive
LinearMap.IsPositive.ne_zero_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E}, T.IsPositive → (T ≠ 0 ↔ ∃ x, 0 < inner 𝕜 (T x) x)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
IsClosed.measurableSet : ∀ {α : Type u_1} {s : Set α} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α],
  IsClosed s → MeasurableSet s
-- Lean.MetavarContext
Lean.MetavarContext.MkBinding.State.mk : Lean.MetavarContext →
  Lean.MacroScope → Lean.NameGenerator → Std.HashMap Lean.ExprStructEq Lean.Expr → Lean.MetavarContext.MkBinding.State
-- Mathlib.Topology.Gluing
TopCat.GlueData.MkCore.mk : {J : Type u} →
  (U : J → TopCat) →
    (V : (i : J) → J → TopologicalSpace.Opens ↑(U i)) →
      (t :
          (i j : J) →
            (TopologicalSpace.Opens.toTopCat (U i)).obj (V i j) ⟶ (TopologicalSpace.Opens.toTopCat (U j)).obj (V j i)) →
        (∀ (i : J), V i i = ⊤) →
          (∀ (i : J), ⇑(CategoryTheory.ConcreteCategory.hom (t i i)) = id) →
            (t_inter :
                ∀ ⦃i j : J⦄ (k : J) (x : ↥(V i j)),
                  ↑x ∈ V i k → ↑((CategoryTheory.ConcreteCategory.hom (t i j)) x) ∈ V j k) →
              (∀ (i j k : J) (x : ↥(V i j)) (h : ↑x ∈ V i k),
                  ↑((CategoryTheory.ConcreteCategory.hom (t j k))
                        ⟨↑((CategoryTheory.ConcreteCategory.hom (t i j)) x), ⋯⟩) =
                    ↑((CategoryTheory.ConcreteCategory.hom (t i k)) ⟨↑x, h⟩)) →
                TopCat.GlueData.MkCore
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.mul_mem : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) (x y : K), x ∈ A → y ∈ A → x * y ∈ A
-- Init.Data.Iterators.Lemmas.Producers.Monadic.List
_private.Init.Data.Iterators.Lemmas.Producers.Monadic.List.0.Std.IterM.toArray_eq_match_step.match_1.splitter : {α β : Type u_1} →
  {m : Type u_1 → Type u_2} →
    (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) →
      (x : Std.IterStep (Std.IterM m β) β) →
        ((it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out)) →
          ((it' : Std.IterM m β) → motive (Std.IterStep.skip it')) → (Unit → motive Std.IterStep.done) → motive x
-- Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd
Measure.ext_of_integral_prod_mul_boundedContinuousFunction : ∀ {ι : Type u_1} {T : Type u_4} {X : ι → Type u_5} {mX : (i : ι) → MeasurableSpace (X i)}
  [inst : (i : ι) → TopologicalSpace (X i)] [∀ (i : ι), BorelSpace (X i)] [∀ (i : ι), HasOuterApproxClosed (X i)]
  {mT : MeasurableSpace T} [inst_3 : TopologicalSpace T] [BorelSpace T] [HasOuterApproxClosed T] [inst_6 : Fintype ι]
  {μ ν : MeasureTheory.Measure (((i : ι) → X i) × T)} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν],
  (∀ (f : (i : ι) → BoundedContinuousFunction (X i) ℝ) (g : BoundedContinuousFunction T ℝ),
      ∫ (p : ((i : ι) → X i) × T), (∏ i, (f i) (p.1 i)) * g p.2 ∂μ =
        ∫ (p : ((i : ι) → X i) × T), (∏ i, (f i) (p.1 i)) * g p.2 ∂ν) →
    μ = ν
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.interSmallerFn.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (m : Std.DTreeMap.Internal.Impl α β) (sofar : { t // t.Balanced })
  (k : α),
  m.interSmallerFn sofar k =
    match m.getEntry? k with
    | some kv' =>
      match Std.DTreeMap.Internal.Impl.insert kv'.fst kv'.snd ↑sofar ⋯ with
      |
      { impl := val, balanced_impl := prop, lb_le_size_impl := lb_le_size_impl, size_impl_le_ub := size_impl_le_ub } =>
        ⟨val, prop⟩
    | none => sofar
-- Mathlib.Algebra.Order.Antidiag.Nat
_private.Mathlib.Algebra.Order.Antidiag.Nat.0.Nat.card_pair_lcm_eq.f_inj : ∀ {n : ℕ} (a : Fin 3 → ℕ) (ha : a ∈ Nat.finMulAntidiag 3 n) (b : Fin 3 → ℕ) (hb : b ∈ Nat.finMulAntidiag 3 n),
  Nat.card_pair_lcm_eq.f✝ a ha = Nat.card_pair_lcm_eq.f✝ b hb → a = b
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.primrec_const : Primrec Nat.Partrec.Code.const
-- Mathlib.RingTheory.Valuation.Basic
Valuation.map_one_sub_of_lt : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀)
  {x : R}, v x < 1 → v (1 - x) = 1
-- Init.MetaTypes
/-- When `true` (default: `true`), the `^` simprocs generate an warning it the exponents are too big.
 -/
Lean.Meta.Simp.Config.warnExponents : Lean.Meta.Simp.Config → Bool
-- Mathlib.Topology.MetricSpace.IsometricSMul
Metric.preimage_add_left_eball : ∀ {G : Type v} [inst : AddGroup G] [inst_1 : PseudoEMetricSpace G] [IsIsometricVAdd G G] (a b : G) (r : ENNReal),
  (fun x => a + x) ⁻¹' Metric.eball b r = Metric.eball (-a + b) r
-- Lean.Meta.Tactic.AuxLemma
Lean.Meta.AuxLemmaKey.mk.inj : ∀ {type : Lean.Expr} {isPrivate defeq : Bool} {type_1 : Lean.Expr} {isPrivate_1 defeq_1 : Bool},
  { type := type, isPrivate := isPrivate, defeq := defeq } =
      { type := type_1, isPrivate := isPrivate_1, defeq := defeq_1 } →
    type = type_1 ∧ isPrivate = isPrivate_1 ∧ defeq = defeq_1
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.smul_eq_C_smul : ∀ {K : Type u} [inst : CommRing K] (x : RatFunc K) (r : K), r • x = Polynomial.C r • x
-- Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
AddChar.sum_apply_eq_zero_iff_ne_zero : ∀ {α : Type u_1} [inst : AddCommGroup α] {a : α} [inst_1 : Finite α], ∑ ψ, ψ a = 0 ↔ a ≠ 0
-- Mathlib.Algebra.Ring.Int.Parity
Int.even_xor_odd' : ∀ (n : ℤ), ∃ k, Xor (n = 2 * k) (n = 2 * k + 1)
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHom.coe_copy : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : AddCommMonoid B] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (f : A →ₗc[R] B) (f' : A → B) (h : f' = ⇑f), ⇑(f.copy f' h) = f'
-- Mathlib.Analysis.Convex.Topology
/-- In a topological vector space, the interior of a convex set is convex.  -/
Convex.interior : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E]
  [ZeroLEOneClass 𝕜] {s : Set E}, Convex 𝕜 s → Convex 𝕜 (interior s)
-- Init.Data.List.Basic
/-- The empty list is a permutation of the empty list: `[] ~ []`.  -/
List.Perm.nil : ∀ {α : Type u}, [].Perm []
-- Lean.Meta.PPGoal
Lean.Meta.getGoalPrefix : Lean.MetavarDecl → String
-- Std.Do.WP.SimpLemmas
Std.Do.WP.throw_lift_OptionT : ∀ {m : Type u → Type v} {sh : Std.Do.PostShape} {ε α : Type u} {e : ε}
  {Q : Std.Do.PostCond α (Std.Do.PostShape.except PUnit.{u + 1} sh)} [inst : Std.Do.WP m sh] [Monad m]
  [inst_2 : MonadExceptOf ε m],
  (Std.Do.wp (MonadExceptOf.throw e)).apply Q =
    (Std.Do.wp (MonadExceptOf.throw e)).apply (fun o => Option.casesOn o (Q.2.1 PUnit.unit) Q.1, Q.2.2)
-- Mathlib.Analysis.InnerProductSpace.Projection.Reflection
Submodule.reflection_sub : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {v w : F},
  ‖v‖ = ‖w‖ → (ℝ ∙ (v - w))ᗮ.reflection v = w
-- Mathlib.Topology.Semicontinuity.Defs
LowerSemicontinuousAt.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace γ]
  [inst_2 : Preorder β] {f : α → β} {g : γ → α} {x : γ},
  LowerSemicontinuousAt f (g x) → ContinuousAt g x → LowerSemicontinuousAt (f ∘ g) x
-- Lean.Meta.Sym.Simp.SimpM
Lean.Meta.Sym.Simp.Config.mk : ℕ → ℕ → Lean.Meta.Sym.Simp.Config
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.fillNones.match_1.eq_1 : ∀ {α : Type u_1} (motive : List (Option α) → List α → Sort u_2) (x : List α) (h_1 : (x : List α) → motive [] x)
  (h_2 : (a : α) → (as : List (Option α)) → (as' : List α) → motive (some a :: as) as')
  (h_3 : (as : List (Option α)) → motive (none :: as) [])
  (h_4 : (as : List (Option α)) → (a : α) → (as' : List α) → motive (none :: as) (a :: as')),
  (match [], x with
    | [], x => h_1 x
    | some a :: as, as' => h_2 a as as'
    | none :: as, [] => h_3 as
    | none :: as, a :: as' => h_4 as a as') =
    h_1 x
-- Batteries.Data.List.Perm
List.Sublist.subperm : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂ → l₁.Subperm l₂
-- Mathlib.Analysis.Calculus.FDeriv.Defs
/-- A function `f` has derivative `f'` at `a` in the sense of *strict differentiability*
if `f x - f y - f' (x - y) = o(x - y)` as `x, y → a`. This form of differentiability is required,
e.g., by the inverse function theorem. Any `C^1` function on a vector space over `ℝ` is strictly
differentiable but this definition works, e.g., for vector spaces over `p`-adic numbers.  -/
HasStrictFDerivAt : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : AddCommGroup E] →
        [inst_2 : Module 𝕜 E] →
          [inst_3 : TopologicalSpace E] →
            {F : Type u_3} →
              [inst_4 : AddCommGroup F] →
                [inst_5 : Module 𝕜 F] → [inst_6 : TopologicalSpace F] → (E → F) → (E →L[𝕜] F) → E → Prop
-- Mathlib.Order.SymmDiff
Codisjoint.bihimp_right : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {a b c : α}, Codisjoint a b → Codisjoint a c → Codisjoint a (bihimp b c)
-- Mathlib.Algebra.Lie.Quotient
LieSubmodule.Quotient.mk_eq_zero : ∀ {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 : LieSubmodule R L M) [inst_5 : LieAlgebra R L]
  [inst_6 : LieModule R L M] {m : M}, (LieSubmodule.Quotient.mk' N) m = 0 ↔ m ∈ N
-- Mathlib.CategoryTheory.Limits.Types.Coequalizers
CategoryTheory.Limits.Types.coequalizerIso_π_comp_hom_apply : ∀ {X Y : Type u} (f g : X ⟶ Y) (x : Y),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Types.coequalizerIso f g).hom)
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.coequalizer.π f g)) x) =
    Function.Coequalizer.mk (⇑(CategoryTheory.ConcreteCategory.hom f)) (⇑(CategoryTheory.ConcreteCategory.hom g)) x
-- Mathlib.RingTheory.Nakayama
/-- **Nakayama's Lemma** - A slightly more general version of (4) in
[Stacks 00DV](https://stacks.math.columbia.edu/tag/00DV).
See also `smul_le_of_le_smul_of_le_jacobson_bot` for the special case when `J = ⊥`.  -/
Submodule.sup_smul_eq_sup_smul_of_le_smul_of_le_jacobson : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I J : Ideal R}
  {N N' : Submodule R M}, N'.FG → I ≤ J.jacobson → N' ≤ N ⊔ I • N' → N ⊔ I • N' = N ⊔ J • N'
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.instCommRingOfCommMonoid : (α : Type u) → [CommMonoid α] → CommRing (FreeAbelianGroup α)
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndep.indep : ∀ {Ω : Type u_1} {ι : Type u_2} {m : ι → MeasurableSpace Ω} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω},
  ProbabilityTheory.iIndep m μ → ∀ {i j : ι}, i ≠ j → ProbabilityTheory.Indep (m i) (m j) μ
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.leadingCoeff_eraseLead_eq_nextCoeff : ∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R}, f.nextCoeff ≠ 0 → f.eraseLead.leadingCoeff = f.nextCoeff
-- Lean.Meta.Tactic.Simp.SimpTheorems
/-- If `e` is a backwards theorem `← thm`, we must ensure the forward theorem is erased
from `d`. See issue #4290
 -/
_private.Lean.Meta.Tactic.Simp.SimpTheorems.0.Lean.Meta.eraseFwdIfBwd : Lean.Meta.SimpTheorems → Lean.Meta.SimpTheorem → Lean.Meta.SimpTheorems
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem?_filter_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {f : α → β → Bool} {k k' : α},
  m.getKey? k = some k' → (Std.HashMap.filter f m)[k]? = Option.filter (fun x => f k' x) m[k]?
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.neighborSet_iSup : ∀ {ι : Sort u_1} {V : Type u} {s : ι → SimpleGraph V} (v : V), (⨆ i, s i).neighborSet v = ⋃ i, (s i).neighborSet v
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- Auxiliary definition for `StronglyMeasurable.of_discrete`.  -/
_private.Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic.0.MeasureTheory.simpleFuncAux : {α : Type u_1} →
  {β : Type u_2} →
    {x : MeasurableSpace α} → [MeasurableSingletonClass α] → (α → β) → (ℕ → α) → ℕ → MeasureTheory.SimpleFunc α β
-- Mathlib.Order.SuccPred.Basic
/-- Not to be confused with `WithTop.pred_bot`, which is about `WithTop.pred`.  -/
WithTop.orderPred_top : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderTop α] [inst_2 : PredOrder α], Order.pred ⊤ = ↑⊤
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
StrictAnti.add_const : ∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f : β → α}
  [AddRightStrictMono α], StrictAnti f → ∀ (c : α), StrictAnti fun x => f x + c
-- Mathlib.LinearAlgebra.Contraction
dualTensorHomEquivOfBasis_toLinearMap : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (b : Module.Basis ι R M)
  [inst_5 : DecidableEq ι] [inst_6 : Fintype ι], ↑(dualTensorHomEquivOfBasis b) = dualTensorHom R M N
-- Mathlib.Data.Complex.Basic
Complex.forall : ∀ {p : ℂ → Prop}, (∀ (x : ℂ), p x) ↔ ∀ (a b : ℝ), p { re := a, im := b }
-- Init.Data.Slice.Notation
Std.Roo.Sliceable.mk : {α : Type u} → {β : outParam (Type v)} → {γ : outParam (Type w)} → (α → Std.Roo β → γ) → Std.Roo.Sliceable α β γ
-- Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Complex.hasDerivAt_log_sub_logTaylor : ∀ (n : ℕ) {z : ℂ},
  1 + z ∈ Complex.slitPlane →
    HasDerivAt (fun z => Complex.log (1 + z) - Complex.logTaylor (n + 1) z) ((-z) ^ n * (1 + z)⁻¹) z
-- Mathlib.Algebra.Order.Star.Basic
IsSelfAdjoint.conjugate_le_conjugate : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  {a b : R}, a ≤ b → ∀ {c : R}, IsSelfAdjoint c → c * a * c ≤ c * b * c
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
ContMDiff.inr : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {M' : Type u_16} [inst_6 : TopologicalSpace M']
  [inst_7 : ChartedSpace H M'] {n : WithTop ℕ∞}, ContMDiff I I n Sum.inr
-- Mathlib.RingTheory.Smooth.NoetherianDescent
_private.Mathlib.RingTheory.Smooth.NoetherianDescent.0.Algebra.Smooth.DescentAux.algebra₀ : (R : Type u_1) →
  [inst : CommRing R] →
    {A : Type u} →
      {B : Type u_2} →
        [inst_1 : CommRing A] →
          [inst_2 : Algebra R A] →
            [inst_3 : CommRing B] →
              [inst_4 : Algebra A B] →
                (D : Algebra.Smooth.DescentAux✝ A B) → Algebra R ↥(Algebra.Smooth.DescentAux.subalgebra✝ R D)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
/-- Same as `IsPushout.of_iso`, but using the data and compatibilities involving
the inverse isomorphisms instead.  -/
CategoryTheory.IsPushout.of_iso' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P}
  {inr : Y ⟶ P},
  CategoryTheory.IsPushout f g inl inr →
    ∀ {Z' X' Y' P' : C} {f' : Z' ⟶ X'} {g' : Z' ⟶ Y'} {inl' : X' ⟶ P'} {inr' : Y' ⟶ P'} (e₁ : Z' ≅ Z) (e₂ : X' ≅ X)
      (e₃ : Y' ≅ Y) (e₄ : P' ≅ P),
      CategoryTheory.CategoryStruct.comp e₁.hom f = CategoryTheory.CategoryStruct.comp f' e₂.hom →
        CategoryTheory.CategoryStruct.comp e₁.hom g = CategoryTheory.CategoryStruct.comp g' e₃.hom →
          CategoryTheory.CategoryStruct.comp e₂.hom inl = CategoryTheory.CategoryStruct.comp inl' e₄.hom →
            CategoryTheory.CategoryStruct.comp e₃.hom inr = CategoryTheory.CategoryStruct.comp inr' e₄.hom →
              CategoryTheory.IsPushout f' g' inl' inr'
-- Std.Data.Internal.Cut
Std.Internal.IsCut.mk : ∀ {α : Type u} {cmp : α → α → Ordering} {cut : α → Ordering},
  (∀ {k k' : α}, cut k' = Ordering.lt → cmp k' k = Ordering.lt → cut k = Ordering.lt) →
    (∀ {k k' : α}, cut k' = Ordering.gt → cmp k' k = Ordering.gt → cut k = Ordering.gt) → Std.Internal.IsCut cmp cut
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.im_star : ∀ {R : Type u_2} {a b : R} [inst : CommRing R] (z : QuadraticAlgebra R a b), (star z).im = -z.im
-- Mathlib.Algebra.Group.Hom.Basic
/-- Given two additive morphisms `f`, `g` to an additive commutative semigroup,
`f + g` is the additive morphism sending `x` to `f x + g x`.  -/
AddHom.instAdd : {M : Type u_2} → {N : Type u_3} → [inst : Add M] → [inst_1 : AddCommSemigroup N] → Add (M →ₙ+ N)
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleConfig.mk.injEq : ∀ (term? : Option Lean.Term) (phase? : Option Aesop.PhaseName) (priority? : Option Aesop.Frontend.Priority)
  (builder? : Option Aesop.Frontend.DBuilderName) (builderOptions : Aesop.RuleBuilderOptions)
  (ruleSets : Aesop.Frontend.RuleSets) (term?_1 : Option Lean.Term) (phase?_1 : Option Aesop.PhaseName)
  (priority?_1 : Option Aesop.Frontend.Priority) (builder?_1 : Option Aesop.Frontend.DBuilderName)
  (builderOptions_1 : Aesop.RuleBuilderOptions) (ruleSets_1 : Aesop.Frontend.RuleSets),
  ({ term? := term?, phase? := phase?, priority? := priority?, builder? := builder?, builderOptions := builderOptions,
        ruleSets := ruleSets } =
      { term? := term?_1, phase? := phase?_1, priority? := priority?_1, builder? := builder?_1,
        builderOptions := builderOptions_1, ruleSets := ruleSets_1 }) =
    (term? = term?_1 ∧
      phase? = phase?_1 ∧
        priority? = priority?_1 ∧ builder? = builder?_1 ∧ builderOptions = builderOptions_1 ∧ ruleSets = ruleSets_1)
-- Mathlib.Topology.Order.Monotone
/-- A monotone right-continuous function is right-continuous in the order-theoretic sense.  -/
Monotone.rightOrdContinuous : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : LinearOrder β] {f : α → β} [inst_4 : TopologicalSpace β] [OrderTopology β],
  Monotone f → (∀ (x : α), ContinuousWithinAt f (Set.Ici x) x) → RightOrdContinuous f
-- Mathlib.Topology.Closure
closure_eq_compl_interior_compl : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, closure s = (interior sᶜ)ᶜ
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
AddSubgroup.instEncodableSubtypeAddOppositeMemOp : {G : Type u_2} → [inst : AddGroup G] → (H : AddSubgroup G) → [Encodable ↥H] → Encodable ↥H.op
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapGrpNatTrans_app_hom_hom : ∀ {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 F' : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] [inst_5 : F'.Monoidal] (f : F ⟶ F')
  (X : CategoryTheory.Grp C), ((CategoryTheory.Functor.mapGrpNatTrans f).app X).hom.hom = f.app X.X
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.eq_natCast_or_omega0_le : ∀ (o : Ordinal.{u_4}), (∃ n, o = ↑n) ∨ Ordinal.omega0 ≤ o
-- Mathlib.Analysis.Normed.Group.Basic
mem_ball_iff_norm : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E] {a b : E} {r : ℝ}, b ∈ Metric.ball a r ↔ ‖b - a‖ < r
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy
CategoryTheory.Limits.FormalCoproduct.instHasLimitWidePullbackShapeToTypeSimplexCategoryOrderHomFinHAddNatLenOfNatWideCospanObjInclFromIsTerminalIncl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C]
  (U : CategoryTheory.Limits.FormalCoproduct C) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (n : SimplexCategory),
  CategoryTheory.Limits.HasLimit
    (CategoryTheory.Limits.WidePullbackShape.wideCospan ((CategoryTheory.Limits.FormalCoproduct.incl C).obj T)
      (fun x => U) fun x => (CategoryTheory.Limits.FormalCoproduct.isTerminalIncl T hT).from U)
-- Mathlib.Algebra.Lie.SemiDirect
/-- The element of K  -/
LieAlgebra.SemiDirectSum.left : {R : Type u_1} →
  [inst : CommRing R] →
    {K : Type u_2} →
      [inst_1 : LieRing K] →
        [inst_2 : LieAlgebra R K] →
          {L : Type u_3} →
            [inst_3 : LieRing L] → [inst_4 : LieAlgebra R L] → {x : L →ₗ⁅R⁆ LieDerivation R K K} → K ⋊⁅x⁆ L → K
-- Mathlib.Topology.OpenPartialHomeomorph.Continuity
OpenPartialHomeomorph.eventually_nhdsWithin' : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {x : X} (p : X → Prop) {s : Set X},
  x ∈ e.source → ((∀ᶠ (y : Y) in nhdsWithin (↑e x) (↑e.symm ⁻¹' s), p (↑e.symm y)) ↔ ∀ᶠ (x : X) in nhdsWithin x s, p x)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
sub_le_sub_iff_right : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddRightMono α] {a b : α} (c : α), a - c ≤ b - c ↔ a ≤ b
-- Mathlib.Analysis.Fourier.AddCircleMulti
/-- The monomials `mFourierLp 2 n` are an orthonormal set in `L²`.  -/
UnitAddTorus.orthonormal_mFourier : ∀ {d : Type u_1} [inst : Fintype d], Orthonormal ℂ (UnitAddTorus.mFourierLp 2)
-- Mathlib.Topology.Homotopy.Lifting
IsCoveringMap.monodromy_eq_of_map_eq : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X}
  (cov : IsCoveringMap p) {x y : X} {γ : Path.Homotopic.Quotient x y} {ex : ↑(p ⁻¹' {x})} {ey : ↑(p ⁻¹' {y})}
  (Γ : Path.Homotopic.Quotient ↑ex ↑ey),
  Γ.map { toFun := p, continuous_toFun := ⋯ } = γ.cast ⋯ ⋯ → cov.monodromy γ ex = ey
-- Mathlib.Order.CompleteLattice.Defs
CompleteSemilatticeSup.toSupSet : {α : Type u_8} → [self : CompleteSemilatticeSup α] → SupSet α
-- Mathlib.Order.SupClosed
infClosed_singleton : ∀ {α : Type u_3} [inst : SemilatticeInf α] {a : α}, InfClosed {a}
-- Mathlib.CategoryTheory.Limits.Preserves.Filtered
CategoryTheory.Limits.comp_reflectsFilteredColimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.ReflectsFilteredColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F]
  [CategoryTheory.Limits.ReflectsFilteredColimitsOfSize.{w, w', v₂, v₃, u₂, u₃} G],
  CategoryTheory.Limits.ReflectsFilteredColimitsOfSize.{w, w', v₁, v₃, u₁, u₃} (F.comp G)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.IsIndex.simplex_fst_le_castSucc_iff : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} {x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N} {d : ℕ}
  {hd : x.dim = d} {l : Fin d},
  SSet.prodStdSimplex.pairingCore.IsIndex x hd l.succ →
    ∀ (i : Fin (d + 1)), (x.cast hd).simplex.1 i ≤ k.castSucc ↔ i < l.succ
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.ordCompare_maxKey_modify_eq : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] {t : Std.TreeMap α β compare} {k : α} {f : β → β}
  {he : (t.modify k f).isEmpty = false}, compare ((t.modify k f).maxKey he) (t.maxKey ⋯) = Ordering.eq
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.coe_list_sum : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddMonoid α] (s : List (Finset α)),
  ↑s.sum = (List.map SetLike.coe s).sum