mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- Composition of two linear maps is a linear map  -/
LinearMap.comp : {R₁ : Type u_2} →
  {R₂ : Type u_3} →
    {R₃ : Type u_4} →
      {M₁ : Type u_9} →
        {M₂ : Type u_10} →
          {M₃ : Type u_11} →
            [inst : Semiring R₁] →
              [inst_1 : Semiring R₂] →
                [inst_2 : Semiring R₃] →
                  [inst_3 : AddCommMonoid M₁] →
                    [inst_4 : AddCommMonoid M₂] →
                      [inst_5 : AddCommMonoid M₃] →
                        {module_M₁ : Module R₁ M₁} →
                          {module_M₂ : Module R₂ M₂} →
                            {module_M₃ : Module R₃ M₃} →
                              {σ₁₂ : R₁ →+* R₂} →
                                {σ₂₃ : R₂ →+* R₃} →
                                  {σ₁₃ : R₁ →+* R₃} →
                                    [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] →
                                      (M₂ →ₛₗ[σ₂₃] M₃) → (M₁ →ₛₗ[σ₁₂] M₂) → M₁ →ₛₗ[σ₁₃] M₃
-- Mathlib.Data.NNRat.Floor
Mathlib.Meta.NormNum.IsNat.natCeil : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorSemiring R] (r : R)
  (m : ℕ), Mathlib.Meta.NormNum.IsNat r m → Mathlib.Meta.NormNum.IsNat ⌈r⌉₊ m
-- Lean.Elab.App
/-- Remove named argument with name `binderName` from `namedArgs`.  -/
Lean.Elab.Term.ElabAppArgs.eraseNamedArg : Lean.Name → Lean.Elab.Term.ElabAppArgs.M Unit
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.sup_support_coeff_finsetProd_le : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} {ι : Type u_6} [inst : SemilatticeSup B] [inst_1 : OrderBot B]
  [inst_2 : CommSemiring R] [inst_3 : AddCommMonoid A] [inst_4 : AddCommMonoid B] [AddLeftMono B] [AddRightMono B]
  {degb : A → B},
  degb 0 ≤ 0 →
    (∀ (a b : A), degb (a + b) ≤ degb a + degb b) →
      ∀ (s : Finset ι) (f : ι → AddMonoidAlgebra R A),
        (∏ i ∈ s, f i).coeff.support.sup degb ≤ ∑ i ∈ s, (f i).coeff.support.sup degb
-- Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexOp
/-- The opposite of subcomplex, as a subcomplex of the opposite simplicial set.  -/
SSet.Subcomplex.op : {X : SSet} → X.Subcomplex → X.op.Subcomplex
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassDivisorAt.div.eq_1 : ∀ {A : Type u_1} [inst : CommRing A] {g : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassDivisorAt I)
  (f : PowerSeries A) [inst_1 : IsPrecomplete I A], H.div f = PowerSeries.mk fun i => ↑(H.divCoeff f i)
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
aemeasurable_derivWithin_Ioi : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] (f : ℝ → F) [CompleteSpace F]
  [inst_3 : MeasurableSpace F] [BorelSpace F] (μ : MeasureTheory.Measure ℝ),
  AEMeasurable (fun x => derivWithin f (Set.Ioi x) x) μ
-- Mathlib.LinearAlgebra.Charpoly.ToMatrix
LinearMap.charpoly_prodMap : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M₁] [inst_2 : Module R M₁]
  [inst_3 : Module.Finite R M₁] [inst_4 : Module.Free R M₁] [inst_5 : AddCommGroup M₂] [inst_6 : Module R M₂]
  [inst_7 : Module.Finite R M₂] [inst_8 : Module.Free R M₂] (f₁ : M₁ →ₗ[R] M₁) (f₂ : M₂ →ₗ[R] M₂),
  (f₁.prodMap f₂).charpoly = f₁.charpoly * f₂.charpoly
-- Mathlib.Order.CompleteLattice.Basic
iInf_eq_dif : ∀ {α : Type u_1} [inst : CompleteLattice α] {p : Prop} [inst_1 : Decidable p] (a : p → α),
  ⨅ (h : p), a h = if h : p then a h else ⊤
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
min_mul : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : LinearOrder α] [MulRightMono α] (a b c : α), min a b * c = min (a * c) (b * c)
-- Mathlib.RepresentationTheory.Coinvariants
/-- The morphism from `ρ` to `toCoinvariants ρ S` induced by the quotient map.  -/
Representation.toCoinvariantsMkQ : {k : Type u_6} →
  {G : Type u_7} →
    {V : Type u_8} →
      [inst : CommRing k] →
        [inst_1 : Group G] →
          [inst_2 : AddCommGroup V] →
            [inst_3 : Module k V] →
              (ρ : Representation k G V) →
                (S : Subgroup G) → [inst_4 : S.Normal] → ρ.IntertwiningMap (ρ.toCoinvariants S)
-- Mathlib.Order.Filter.Map
Filter.comap_le_iff_le_kernMap : ∀ {α : Type u_1} {β : Type u_2} {g : Filter β} {m : α → β} {f : Filter α}, Filter.comap m g ≤ f ↔ g ≤ Filter.kernMap m f
-- Std.Async.System
Std.Async.System.CPUTimes.mk : Std.Time.Millisecond.Offset →
  Std.Time.Millisecond.Offset →
    Std.Time.Millisecond.Offset → Std.Time.Millisecond.Offset → Std.Time.Millisecond.Offset → Std.Async.System.CPUTimes
-- Mathlib.Algebra.Star.MonoidHom
/-- By definition, a star monoid homomorphism preserves the `star` operation.  -/
StarMonoidHom.map_star' : ∀ {A : Type u_6} {B : Type u_7} [inst : Monoid A] [inst_1 : Star A] [inst_2 : Monoid B] [inst_3 : Star B]
  (self : A →⋆* B) (a : A), (↑self.toMonoidHom).toFun (star a) = star ((↑self.toMonoidHom).toFun a)
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.ofRat_div : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_2}
  [inst_3 : DivisionRing β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] (x y : β),
  CauSeq.Completion.ofRat (x / y) = CauSeq.Completion.ofRat x / CauSeq.Completion.ofRat y
-- Mathlib.Analysis.Convex.Between
Wbtw.trans_expand_right : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] {w x y z : P},
  Wbtw R w x y → Wbtw R x y z → x ≠ y → Wbtw R w y z
-- Mathlib.LinearAlgebra.Matrix.Nondegenerate
_private.Mathlib.LinearAlgebra.Matrix.Nondegenerate.0.Matrix.SeparatingLeft.of_det_mem_nonZeroDivisors : ∀ {m : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : Fintype m] [inst_2 : DecidableEq m] {M : Matrix m m R},
  M.det ∈ nonZeroDivisors R → M.SeparatingLeft
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
/-- The inverse of `tensorμ`.  -/
CategoryTheory.MonoidalCategory.tensorδ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] →
        (X₁ X₂ Y₁ Y₂ : C) →
          CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ Y₁)
              (CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ Y₂) ⟶
            CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂)
              (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₁ Y₂)
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanced_balance! : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β},
  l.Balanced →
    r.Balanced →
      Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l.size r.size ∨
          Std.DTreeMap.Internal.Impl.BalanceLErasePrecond r.size l.size →
        (Std.DTreeMap.Internal.Impl.balance! k v l r).Balanced
-- Mathlib.Topology.Category.UniformSpace
CpltSepUniformSpace.instCoeSortType : CoeSort CpltSepUniformSpace (Type u)
-- Mathlib.Algebra.Group.Equiv.Opposite
/-- The 'unopposite' of an iso `αᵃᵒᵖ ≃+ βᵃᵒᵖ`. Inverse to `AddEquiv.op`.  -/
AddEquiv.unop : {α : Type u_3} → {β : Type u_4} → [inst : Add α] → [inst_1 : Add β] → αᵃᵒᵖ ≃+ βᵃᵒᵖ ≃ (α ≃+ β)
-- Mathlib.Analysis.Normed.Lp.lpSpace
memℓp_gen_iff'' : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i},
  0 < p.toReal → (Memℓp f p ↔ ∃ C, 0 ≤ C ∧ ∀ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C)
-- Lean.Environment
Lean.Kernel.Exception.invalidProj.inj : ∀ {env : Lean.Kernel.Environment} {lctx : Lean.LocalContext} {proj : Lean.Expr} {env_1 : Lean.Kernel.Environment}
  {lctx_1 : Lean.LocalContext} {proj_1 : Lean.Expr},
  Lean.Kernel.Exception.invalidProj env lctx proj = Lean.Kernel.Exception.invalidProj env_1 lctx_1 proj_1 →
    env = env_1 ∧ lctx = lctx_1 ∧ proj = proj_1
-- Mathlib.RepresentationTheory.Action
Representation.linearizeMap_single : ∀ {k : Type u} {G : Type v} [inst : Monoid G] [inst_1 : Semiring k] {X Y : Action (Type w) G} (f : X ⟶ Y) (x : X.V)
  (r : k),
  (Representation.linearizeMap f) (MonoidAlgebra.single x r) =
    MonoidAlgebra.single ((CategoryTheory.ConcreteCategory.hom f.hom) x) r
-- Mathlib.Algebra.Group.Defs
IsCancelMul.mk : ∀ {G : Type u} [inst : Mul G] [toIsLeftCancelMul : IsLeftCancelMul G] [toIsRightCancelMul : IsRightCancelMul G],
  IsCancelMul G
-- Mathlib.Algebra.BigOperators.Ring.Multiset
Commute.multiset_sum_right : ∀ {R : Type u_4} [inst : NonUnitalNonAssocSemiring R] (s : Multiset R) (a : R), (∀ b ∈ s, Commute a b) → Commute a s.sum
-- Init.Data.Array.Bootstrap
Array.foldlM_toList.aux : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [inst : Monad m] {f : β → α → m β} {xs : Array α} {i j : ℕ},
  xs.size ≤ i + j → ∀ {b : β}, Array.foldlM.loop f xs xs.size ⋯ i j b = List.foldlM f b (List.drop j xs.toList)
-- Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
min_add_add_left : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : Add α] [AddLeftMono α] (a b c : α), min (a + b) (a + c) = a + min b c
-- Mathlib.Topology.MetricSpace.HausdorffDistance
Metric.infEDist_eq_top_iff : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {x : α}, Metric.infEDist x s = ⊤ ↔ s = ∅
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.coe_neg : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β]
  (f : BoundedContinuousFunction α β), ⇑(-f) = -⇑f
-- Lean.Meta.Sym.DSimp.DSimpM
Lean.Meta.Sym.DSimp.pre : Lean.Meta.Sym.DSimp.DSimproc
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.entryAtIdx?_eq_getElem? : ∀ {α : Type u} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β},
  t.Balanced →
    ∀ {i : ℕ}, Std.DTreeMap.Internal.Impl.Const.entryAtIdx? t i = Option.map (fun x => (x.fst, x.snd)) t.toListModel[i]?
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.arrowSucc_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] [inst_2 : SuccOrder J]
  {j : J} (F : CategoryTheory.Functor (↑(Set.Iic j)) C) (i : J) (hi : i < j),
  CategoryTheory.SmallObject.SuccStruct.arrowSucc F i hi =
    CategoryTheory.SmallObject.SuccStruct.arrowMap F i (Order.succ i) ⋯ ⋯
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.cond.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match false with
    | true => h_1 ()
    | false => h_2 ()) =
    h_2 ()
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.HasPointwiseLeftKanExtension.of_iso : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  {L L' : CategoryTheory.Functor C D} {F F' : CategoryTheory.Functor C H} [L.HasPointwiseLeftKanExtension F]
  (e₁ : L ≅ L') (e₂ : F ≅ F'), L'.HasPointwiseLeftKanExtension F'
-- Mathlib.Algebra.Lie.Ideal
LieIdeal.top_toLieSubalgebra : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  LieIdeal.toLieSubalgebra R L ⊤ = ⊤
-- Mathlib.Data.Num.Lemmas
Num.add_of_nat : ∀ (m n : ℕ), ↑(m + n) = ↑m + ↑n
-- Mathlib.FieldTheory.AlgebraicClosure
/-- If `i` is an `F`-algebra homomorphism from `E` to `K`, then `i x` is contained in
`algebraicClosure F K` if and only if `x` is contained in `algebraicClosure F E`.  -/
map_mem_algebraicClosure_iff : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type u_3}
  [inst_3 : Field K] [inst_4 : Algebra F K] (i : E →ₐ[F] K) {x : E},
  i x ∈ algebraicClosure F K ↔ x ∈ algebraicClosure F E
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithTerminal.coneEquiv_inverse_obj_pt_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Over X)}
  (t : CategoryTheory.Limits.Cone (CategoryTheory.WithTerminal.liftFromOver.obj K)),
  (CategoryTheory.WithTerminal.coneEquiv.inverse.obj t).pt.left = t.pt
-- Init.Data.Int.Order
Int.neg_add_lt_right_of_lt_add : ∀ {a b c : ℤ}, a < b + c → -c + a < b
-- Mathlib.Order.Filter.Lift
Filter.prod_lift_lift : ∀ {α₁ : Type u_5} {α₂ : Type u_6} {β₁ : Type u_7} {β₂ : Type u_8} {f₁ : Filter α₁} {f₂ : Filter α₂}
  {g₁ : Set α₁ → Filter β₁} {g₂ : Set α₂ → Filter β₂},
  Monotone g₁ → Monotone g₂ → f₁.lift g₁ ×ˢ f₂.lift g₂ = f₁.lift fun s => f₂.lift fun t => g₁ s ×ˢ g₂ t
-- Mathlib.LinearAlgebra.Dimension.RankNullity
LinearMap.lift_rank_eq_of_surjective : ∀ {R : Type u_1} {M : Type u} {M' : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup M']
  [inst_3 : Module R M] [inst_4 : Module R M'] [HasRankNullity.{u, u_1} R] {f : M →ₗ[R] M'},
  Function.Surjective ⇑f →
    Cardinal.lift.{v, u} (Module.rank R M) =
      Cardinal.lift.{u, v} (Module.rank R M') + Cardinal.lift.{v, u} (Module.rank R ↥f.ker)
-- Mathlib.Topology.CompactOpen
/-- For any subset `s` of `X`, the restriction of continuous functions to `s` is continuous
as a function from `C(X, Y)` to `C(s, Y)` with their respective compact-open topologies.  -/
ContinuousMap.continuous_restrict : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (s : Set X),
  Continuous fun F => ContinuousMap.restrict s F
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
/-- If `g * q + r = g * q' + r'` for some power series `q`, `q'` and some polynomials `r`, `r'`
whose degrees are `< n`, then `q = q'` and `r = r'` are all zero.
This implies the uniqueness of Weierstrass division.  -/
PowerSeries.IsWeierstrassDivisorAt.eq_of_mul_add_eq_mul_add : ∀ {A : Type u_1} [inst : CommRing A] {g : PowerSeries A} {I : Ideal A},
  g.IsWeierstrassDivisorAt I →
    ∀ [IsHausdorff I A] {q q' : PowerSeries A} {r r' : Polynomial A},
      r.degree < ↑((PowerSeries.map (Ideal.Quotient.mk I)) g).order.toNat →
        r'.degree < ↑((PowerSeries.map (Ideal.Quotient.mk I)) g).order.toNat →
          g * q + ↑r = g * q' + ↑r' → q = q' ∧ r = r'
-- Mathlib.Data.Multiset.Bind
Multiset.add_bind : ∀ {α : Type u_1} {β : Type v} (s t : Multiset α) (f : α → Multiset β), (s + t).bind f = s.bind f + t.bind f
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey!_insert_le_minKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → t.isEmpty = false → ∀ {k : α} {v : β}, (cmp (t.insert k v).minKey! t.minKey!).isLE = true
-- Mathlib.NumberTheory.Dioph
Poly.sumsq.eq_1 : ∀ {α : Type u_1}, Poly.sumsq [] = 0
-- Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory
SemiSimplexCategory.hom_ext : ∀ {a b : SemiSimplexCategory} {f g : a ⟶ b}, SemiSimplexCategory.homEquiv f = SemiSimplexCategory.homEquiv g → f = g
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.map_map_equiv : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} {δ : α → Type w'} (m : Std.DHashMap.Internal.Raw₀ α β)
  {f : (a : α) → β a → γ a} {g : (a : α) → γ a → δ a},
  (↑(Std.DHashMap.Internal.Raw₀.map g (Std.DHashMap.Internal.Raw₀.map f m))).Equiv
    ↑(Std.DHashMap.Internal.Raw₀.map (fun k v => g k (f k v)) m)
-- Mathlib.Topology.MetricSpace.IsometricSMul
/-- **Alias** of `Metric.preimage_add_left_closedEBall`. -/
EMetric.preimage_add_left_closedBall : ∀ {G : Type v} [inst : AddGroup G] [inst_1 : PseudoEMetricSpace G] [IsIsometricVAdd G G] (a b : G) (r : ENNReal),
  (fun x => a + x) ⁻¹' Metric.closedEBall b r = Metric.closedEBall (-a + b) r
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.mem_map : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : NonUnitalNonAssocSemiring B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : FunLike F A B]
  [inst_6 : NonUnitalAlgHomClass F R A B] {S : NonUnitalSubalgebra R A} {f : F} {y : B},
  y ∈ NonUnitalSubalgebra.map f S ↔ ∃ x ∈ S, f x = y
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get?_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {a k : α} {v : β k},
  (t.insert k v).get? a = if h : cmp k a = Ordering.eq then some (cast ⋯ v) else t.get? a
-- Mathlib.Data.Finsupp.Basic
Finsupp.restrictSupportEquiv_symm_single : ∀ {α : Type u_1} (s : Set α) (M : Type u_12) [inst : AddCommMonoid M] (a : ↑s) (x : M),
  ↑((Finsupp.restrictSupportEquiv s M).symm fun₀ | a => x) = fun₀ | ↑a => x
-- Mathlib.Order.DirectedInverseSystem
DirectedSystem.map_map : ∀ {ι : Type u_1} {inst : Preorder ι} {F : ι → Type u_4} {f : ⦃i j : ι⦄ → i ≤ j → F i → F j} [self : DirectedSystem F f]
  ⦃k j i : ι⦄ (hij : i ≤ j) (hjk : j ≤ k) (x : F i), f hjk (f hij x) = f ⋯ x
-- Lean.Compiler.IR.Basic
Lean.IR.Expr.ap.sizeOf_spec : ∀ (x : Lean.IR.VarId) (ys : Array Lean.IR.Arg), sizeOf (Lean.IR.Expr.ap x ys) = 1 + sizeOf x + sizeOf ys
-- Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
ofCompactSupport_mem : ∀ {α : Type u_1} {γ : Type u_2} [inst : TopologicalSpace α] [inst_1 : NonUnitalNormedRing γ] (g : α → γ)
  (hg₁ : Continuous g) (hg₂ : HasCompactSupport g), ofCompactSupport g hg₁ hg₂ ∈ compactlySupported α γ
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
OpenPartialHomeomorph.MDifferentiable.symm : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {e : OpenPartialHomeomorph M M'},
  OpenPartialHomeomorph.MDifferentiable I I' e → OpenPartialHomeomorph.MDifferentiable I' I e.symm
-- Mathlib.Order.RelClasses
Set.not_unbounded_iff : ∀ {α : Type u} {r : α → α → Prop} (s : Set α), ¬Set.Unbounded r s ↔ Set.Bounded r s
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.comp_sub : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  [inst_10 : AddCommGroup U] [inst_11 : Module R U] [inst_12 : TopologicalSpace U] [inst_13 : IsTopologicalAddGroup U]
  {π₁ : ContRepresentation R G V} {π₂ : ContRepresentation R G W} {π₃ : ContRepresentation R G U}
  (f : ContIntertwiningMap π₂ π₃) (g h : ContIntertwiningMap π₁ π₂), f.comp (g - h) = f.comp g - f.comp h
-- Mathlib.Analysis.Complex.Basic
/-- The complex-conjugation function from `ℂ` to itself is an isometric linear equivalence.  -/
Complex.conjLIE : ℂ ≃ₗᵢ[ℝ] ℂ
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.ext : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R]
  {s t : HahnSeries.SummableFamily Γ R α}, (∀ (a : α), s a = t a) → s = t
-- Mathlib.Data.Tree.Traversable
BinaryTree.comp_traverse : ∀ {α : Type u_1} {F : Type u → Type v} {G : Type v → Type w} [inst : Applicative F] [inst_1 : Applicative G]
  [LawfulApplicative G] {β : Type v} {γ : Type u} (f : β → F γ) (g : α → G β) (t : BinaryTree α),
  BinaryTree.traverse (Functor.Comp.mk ∘ (fun x => f <$> x) ∘ g) t =
    Functor.Comp.mk ((fun x => BinaryTree.traverse f x) <$> BinaryTree.traverse g t)
-- Mathlib.Algebra.Ring.ULift
ULift.down_natCast : ∀ {R : Type u} [inst : NatCast R] (n : ℕ), (↑n).down = ↑n
-- Mathlib.Algebra.Category.Grp.Limits
GrpCat.forget_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget GrpCat)
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
QuadraticMap.posDef_pi_iff : ∀ {ι : Type u_1} {R : Type u_2} {Mᵢ : ι → Type u_8} [inst : CommSemiring R] [inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)]
  [inst_2 : (i : ι) → Module R (Mᵢ i)] {P : Type u_10} [inst_3 : Fintype ι] [inst_4 : AddCommMonoid P]
  [inst_5 : PartialOrder P] [IsOrderedAddMonoid P] [inst_7 : Module R P] {Q : (i : ι) → QuadraticMap R (Mᵢ i) P},
  (QuadraticMap.pi Q).PosDef ↔ ∀ (i : ι), (Q i).PosDef
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size_insertIfNew : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β}, (m.insertIfNew k v).size = if k ∈ m then m.size else m.size + 1
-- Mathlib.Topology.UnitInterval
unitInterval.half_le_symm_iff : ∀ (t : ↑unitInterval), 1 / 2 ≤ ↑(unitInterval.symm t) ↔ ↑t ≤ 1 / 2
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
SSet.chainComplexMap_PInfty_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] {X Y : SSet} (f : X ⟶ Y) (R : C) {Z : ChainComplex C ℕ}
  (h :
    AlgebraicTopology.AlternatingFaceMapComplex.obj
        (((CategoryTheory.SimplicialObject.whiskering (Type w) C).obj (CategoryTheory.Limits.sigmaConst.obj R)).obj Y) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap f R)
      (CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty h) =
    CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty
      (CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap f R) h)
-- Mathlib.ModelTheory.Graph
FirstOrder.Language.Theory.simpleGraph_model_iff : ∀ {V : Type u} [inst : FirstOrder.Language.graph.Structure V],
  V ⊨ FirstOrder.Language.Theory.simpleGraph ↔
    (Std.Irrefl fun x y => FirstOrder.Language.Structure.RelMap FirstOrder.Language.adj ![x, y]) ∧
      Std.Symm fun x y => FirstOrder.Language.Structure.RelMap FirstOrder.Language.adj ![x, y]
-- Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Set.InvOn.one_sub_one_add_inv : Set.InvOn (fun x => 1 - (1 + x)⁻¹) (fun x => x * (1 - x)⁻¹) {x | x < 1} {x | x < 1}
-- Lean.Structure
/-- If `baseStructName` is an ancestor structure for `structName`, then returns a sequence of projection functions
to go from `structName` to `baseStructName`. Returns `[]` if `baseStructName == structName`.
 -/
Lean.getPathToBaseStructure? : Lean.Environment → Lean.Name → Lean.Name → Option (List Lean.Name)
-- Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing
IsDiscreteValuationRing.isRankOneDiscrete : ∀ (A : Type u_1) (K : Type u_2) [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : IsDiscreteValuationRing A]
  [inst_3 : Field K] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K],
  (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal A)).IsRankOneDiscrete
-- Mathlib.RingTheory.NoetherNormalization
/-- `hom1 f I` is integral.  -/
_private.Mathlib.RingTheory.NoetherNormalization.0.NoetherNormalization.hom1_isIntegral : ∀ {k : Type u_1} [inst : Field k] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) k) (I : Ideal (MvPolynomial (Fin (n + 1)) k)),
  f ≠ 0 → f ∈ I → (NoetherNormalization.hom1✝ f I).IsIntegral
-- Mathlib.Algebra.Order.Sub.Defs
/-- Weaker version of `AddLECancellable.tsub_eq_of_eq_add` assuming that `a = c + b` itself is
cancellable rather than `b`.  -/
AddLECancellable.tsub_eq_of_eq_add' : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b c : α}
  [AddLeftMono α], AddLECancellable a → a = c + b → a - b = c
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.apply_ne_zero_iff : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommMonoidWithZero R'] [Nontrivial R']
  {χ : MulChar R R'} {a : R}, χ a ≠ 0 ↔ IsUnit a
-- Mathlib.Analysis.Normed.Group.Basic
enorm_ne_zero' : ∀ {E : Type u_8} [inst : TopologicalSpace E] [inst_1 : ENormedMonoid E] {a : E}, ‖a‖ₑ ≠ 0 ↔ a ≠ 1