mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.IsStableUnderTransfiniteCompositionOfShape.of_isStableUnderColimitsOfShape.mem_map_bot_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {J : Type w}
  [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J] [inst_4 : WellFoundedLT J] {X Y : C} {f : X ⟶ Y}
  (hf : W.TransfiniteCompositionOfShape J f) [W.IsMultiplicative],
  (∀ (J : Type w) [inst_6 : LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J],
      W.IsStableUnderColimitsOfShape J) →
    ∀ {j : J} (g : ⊥ ⟶ j), W (hf.F.map g)
-- Mathlib.MeasureTheory.Function.UniformIntegrable
/-- Suppose `f` is a sequence of functions that converges a.e. to `g`. If `f` is
`UniformIntegrable`, then `g` is in `Lp`.  -/
MeasureTheory.UniformIntegrable.memLp_of_ae_tendsto : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {p : ENNReal} {κ : Type u_4} {u : Filter κ} [u.NeBot] [u.IsCountablyGenerated] {f : κ → α → β} {g : α → β},
  MeasureTheory.UniformIntegrable f p μ →
    (∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) u (nhds (g x))) → MeasureTheory.MemLp g p μ
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
/-- A cone postcomposed with the inverse of a natural isomorphism is a weak limit cone
if and only if the original cone is.
 -/
CategoryTheory.Limits.IsWeakLimit.postcompose_inv_iff_of_iso : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {C : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_3, u_3} C] {F G : CategoryTheory.Functor J C} (α : F ≅ G)
  (c : CategoryTheory.Limits.Cone G),
  Nonempty (CategoryTheory.Limits.IsWeakLimit ((CategoryTheory.Limits.Cone.postcompose α.inv).obj c)) ↔
    Nonempty (CategoryTheory.Limits.IsWeakLimit c)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.mem_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α (fun x => Unit) cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp],
  t.WF → ∀ {l : List α} {k : α}, k ∈ Std.DTreeMap.Raw.Const.insertManyIfNewUnit t l ↔ k ∈ t ∨ l.contains k = true
-- Mathlib.Data.Set.Finite.Basic
Set.infinite_of_injective_forall_mem : ∀ {α : Type u} {β : Type v} [Infinite α] {s : Set β} {f : α → β},
  Function.Injective f → (∀ (x : α), f x ∈ s) → s.Infinite
-- Init.Data.Vector.Find
Vector.findSome?_isSome_iff : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → Option β} {xs : Vector α n},
  (Vector.findSome? f xs).isSome = true ↔ ∃ x ∈ xs, (f x).isSome = true
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.comp_hom' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {M N K : CategoryTheory.Comon C} (f : M ⟶ N) (g : N ⟶ K),
  (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
-- Mathlib.LinearAlgebra.QuadraticForm.Radical
/-- Over a field of characteristic different from `2`,
the radical of a weighted-sum-of-squares quadratic form is the number of zero weights.  -/
QuadraticForm.radical_weightedSumSquares : ∀ {𝕜 : Type u_1} {ι : Type u_2} [inst : Field 𝕜] [NeZero 2] [inst_2 : Fintype ι] {w : ι → 𝕜},
  (QuadraticMap.weightedSumSquares 𝕜 w).radical = Pi.spanSubset 𝕜 {i | w i = 0}
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsAddFundamentalDomain.integral_eq_tsum' : ∀ {G : Type u_1} {α : Type u_3} {E : Type u_5} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α]
  [inst_3 : NormedAddCommGroup E] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableConstVAdd G α]
  [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] [inst_7 : NormedSpace ℝ E],
  MeasureTheory.IsAddFundamentalDomain G s μ →
    ∀ (f : α → E), MeasureTheory.Integrable f μ → ∫ (x : α), f x ∂μ = ∑' (g : G), ∫ (x : α) in s, f (-g +ᵥ x) ∂μ
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyMapData.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        {φ : S₁ ⟶ S₂} →
          {h₁ : S₁.RightHomologyData} →
            {h₂ : S₂.RightHomologyData} →
              (φQ : h₁.Q ⟶ h₂.Q) →
                (φH : h₁.H ⟶ h₂.H) →
                  autoParam (CategoryTheory.CategoryStruct.comp h₁.p φQ = CategoryTheory.CategoryStruct.comp φ.τ₂ h₂.p)
                      CategoryTheory.ShortComplex.RightHomologyMapData.commp._autoParam →
                    autoParam
                        (CategoryTheory.CategoryStruct.comp φQ h₂.g' = CategoryTheory.CategoryStruct.comp h₁.g' φ.τ₃)
                        CategoryTheory.ShortComplex.RightHomologyMapData.commg'._autoParam →
                      autoParam
                          (CategoryTheory.CategoryStruct.comp φH h₂.ι = CategoryTheory.CategoryStruct.comp h₁.ι φQ)
                          CategoryTheory.ShortComplex.RightHomologyMapData.commι._autoParam →
                        CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂
-- Init.Data.Range.Polymorphic.Internal.SignedBitVec
_private.Init.Data.Range.Polymorphic.Internal.SignedBitVec.0.BitVec.Signed.rotate_eq_iff : ∀ {n : ℕ} {x y : BitVec n}, BitVec.Signed.rotate✝ x = y ↔ x = BitVec.Signed.rotate✝ y
-- Mathlib.Analysis.InnerProductSpace.Positive
/-- `U.starProjection = V.starProjection` iff `U = V`.  -/
Submodule.starProjection_inj : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {U V : Submodule 𝕜 E} [inst_3 : U.HasOrthogonalProjection] [inst_4 : V.HasOrthogonalProjection],
  U.starProjection = V.starProjection ↔ U = V
-- Mathlib.Order.Heyting.Hom
BiheytingHom.id_comp : ∀ {α : Type u_2} {β : Type u_3} [inst : BiheytingAlgebra α] [inst_1 : BiheytingAlgebra β] (f : BiheytingHom α β),
  (BiheytingHom.id β).comp f = f
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHom.toInfTopHom : {α : Type u_6} →
  {β : Type u_7} →
    [inst : Lattice α] →
      [inst_1 : Lattice β] →
        [inst_2 : BoundedOrder α] → [inst_3 : BoundedOrder β] → BoundedLatticeHom α β → InfTopHom α β
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
SSet.Edge.map_id : ∀ {X Y : SSet} (x₀ : X.obj (Opposite.op { len := 0 })) (f : X ⟶ Y),
  (SSet.Edge.id x₀).map f = SSet.Edge.id ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := 0 }))) x₀)
-- Std.Data.String.ToNat
_private.Std.Data.String.ToNat.0.noRepetition_iff : ∀ {α : Type u} {a : α} {l : List α}, NoRepetition✝ a l ↔ ¬[a, a] <:+: l
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
/-- A binary convex combination with weight 1 on the first point returns the first point.  -/
Convexity.convexCombPair_one : ∀ {R : Type u_1} {M : Type u_3} [inst : PartialOrder R] [inst_1 : Semiring R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R M] {x y : M}, Convexity.convexCombPair 1 0 ⋯ ⋯ ⋯ x y = x
-- Init.Data.Float.Model.Unpacked.Sign
Float.Model.UnpackedFloat.Sign.instDiv : Div Float.Model.UnpackedFloat.Sign
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
EisensteinSeries.r1.eq_1 : ∀ (z : UpperHalfPlane), EisensteinSeries.r1 z = z.im ^ 2 / (z.re ^ 2 + z.im ^ 2)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.equiv_emptyWithCapacity_iff_isEmpty : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  (↑m).WF → ∀ {c : ℕ}, (↑m).Equiv ↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity c) ↔ (↑m).isEmpty = true
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- The bijection of `Cofork.IsColimit.homIso` is natural in `Z`.  -/
CategoryTheory.Limits.Cofork.IsColimit.homIso_natural : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {t : CategoryTheory.Limits.Cofork f g}
  {Z Z' : C} (q : Z ⟶ Z') (ht : CategoryTheory.Limits.IsColimit t) (k : t.pt ⟶ Z),
  ↑((CategoryTheory.Limits.Cofork.IsColimit.homIso ht Z') (CategoryTheory.CategoryStruct.comp k q)) =
    CategoryTheory.CategoryStruct.comp (↑((CategoryTheory.Limits.Cofork.IsColimit.homIso ht Z) k)) q
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.volume_pi_Ico_toReal : ∀ {ι : Type u_1} [inst : Fintype ι] {a b : ι → ℝ},
  a ≤ b → (MeasureTheory.volume (Set.univ.pi fun i => Set.Ico (a i) (b i))).toReal = ∏ i, (b i - a i)
-- Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
abs_setIntegral_mulExpNegMulSq_comp_sub_le_mul_measure : ∀ {E : Type u_1} [inst : TopologicalSpace E] [inst_1 : MeasurableSpace E] [BorelSpace E] {P : MeasureTheory.Measure E}
  [MeasureTheory.IsFiniteMeasure P] {ε : ℝ} {K : Set E},
  IsCompact K →
    MeasurableSet K →
      ∀ (f g : C(E, ℝ)) {δ : ℝ},
        0 < ε →
          (∀ x ∈ K, |g x - f x| < δ) →
            |∫ (x : E) in K, ε.mulExpNegMulSq (g x) ∂P - ∫ (x : E) in K, ε.mulExpNegMulSq (f x) ∂P| ≤ δ * (P K).toReal
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.add_right_inj : ∀ {α : Type u} [inst : Add α] {x y z : WithTop α} [IsRightCancelAdd α], z ≠ ⊤ → (x + z = y + z ↔ x = y)
-- Mathlib.Algebra.Group.Units.Defs
Units.instCommGroupUnits.eq_1 : ∀ {α : Type u_1} [inst : CommMonoid α], Units.instCommGroupUnits = { toGroup := Units.instGroup, mul_comm := ⋯ }
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.Adj.ne : ∀ {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} {u v : V}, H.Adj u v → u ≠ v
-- Mathlib.FieldTheory.RatFunc.Degree
RatFunc.intDegree_add_le : ∀ {K : Type u} [inst : Field K] {x y : RatFunc K}, y ≠ 0 → x + y ≠ 0 → (x + y).intDegree ≤ max x.intDegree y.intDegree
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKeyD_insertIfNew : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k a fallback : α} {v : β k},
  (m.insertIfNew k v).getKeyD a fallback = if (k == a) = true ∧ k ∉ m then k else m.getKeyD a fallback
-- Lean.Server.References
/-- Imports as they occurred in the module.  -/
Lean.Server.DirectImports.ordered : Lean.Server.DirectImports → Array Lean.Server.ModuleImport
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.currying_inverse_obj_obj_obj : ∀ {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) E) (X : C) (Y : D),
  ((CategoryTheory.Functor.currying.inverse.obj F).obj X).obj Y = F.obj (X, Y)
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
/-- The product `x * r`, `r : ℚ`, `r ≠ 0`, is a Liouville number with exponent `p` if and only if
`x` satisfies the same condition.  -/
LiouvilleWith.mul_rat_iff : ∀ {p x : ℝ} {r : ℚ}, r ≠ 0 → (LiouvilleWith p (x * ↑r) ↔ LiouvilleWith p x)
-- Batteries.Control.Nondet.Basic
/-- Filter a nondeterministic value using a monadic predicate.  -/
Nondet.filterM : {σ : Type} →
  {m : Type → Type} →
    [Monad m] → [inst : Lean.MonadBacktrack σ m] → {α : Type} → (α → m (ULift.{0, 0} Bool)) → Nondet m α → Nondet m α
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Hom.addEquivCongrRight.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M N : C} [inst_2 : CategoryTheory.AddMonObj M] [inst_3 : CategoryTheory.AddMonObj N] (e : M ≅ N)
  [inst_4 : CategoryTheory.IsAddMonHom e.hom] (X : C),
  CategoryTheory.Hom.addEquivCongrRight e X =
    ((CategoryTheory.yonedaAddMon.mapIso (CategoryTheory.AddMon.mkIso' e)).app (Opposite.op X)).addMonCatIsoToAddEquiv
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.snd_prod : ∀ {R : Type u} [inst : Monoid R] {A : Type v} {B : Type w} {C : Type w₁} [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : NonUnitalNonAssocSemiring C]
  [inst_5 : DistribMulAction R B] [inst_6 : DistribMulAction R C] (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C),
  (NonUnitalAlgHom.snd R B C).comp (f.prod g) = g
-- Mathlib.Algebra.Algebra.Basic
Module.IsTorsionFree.of_faithfulSMul : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [FaithfulSMul R A] [inst_4 : Semiring S] [inst_5 : Module S R] [inst_6 : Module S A] [IsScalarTower S R A]
  [Module.IsTorsionFree S A], Module.IsTorsionFree S R
-- Init.Data.Int.DivMod.Lemmas
Int.tdiv_left_inj : ∀ {a b d : ℤ}, d ∣ a → d ∣ b → (a.tdiv d = b.tdiv d ↔ a = b)
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
measurableSet_generateFrom_of_mem_supClosure : ∀ {α : Type u_1} {s : Set (Set α)} {t : Set α}, t ∈ supClosure s → MeasurableSet t
-- Init.Data.List.Pairwise
List.getElem!_inj : ∀ {α : Type u_1} {i j : ℕ} [inst : Inhabited α] {xs : List α},
  i < xs.length → j < xs.length → xs.Nodup → (xs[i]! = xs[j]! ↔ i = j)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.Monomial.nil_toFun : ∀ {coef : ℝ} {basis : Tactic.ComputeAsymptotics.Basis}, { coef := coef, unit := [] }.toFun basis = fun x => coef
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.isEmpty_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, (t.insert k).isEmpty = false
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.Point.mk_ne_zero : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} [inst_1 : Nontrivial R] {X Y : R}
  (h : W'.NonsingularLift ⟦![X, Y, 1]⟧), { point := ⟦![X, Y, 1]⟧, nonsingular := h } ≠ 0
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RooSliceData : (α : Type u) → [Ord α] → Type u
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.coeff_mul_left_one_sub_of_lt_order : ∀ {σ : Type u_1} {R : Type u_3} [inst : Ring R] {f g : MvPowerSeries σ R} (d : σ →₀ ℕ),
  ↑(Finsupp.degree d) < g.order → (MvPowerSeries.coeff d) (f * (1 - g)) = (MvPowerSeries.coeff d) f
-- Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
MeasureTheory.projectiveFamilyContent_eq : ∀ {ι : Type u_1} {α : ι → Type u_2} {mα : (i : ι) → MeasurableSpace (α i)}
  {P : (J : Finset ι) → MeasureTheory.Measure ((j : ↥J) → α ↑j)} {s : Set ((i : ι) → α i)}
  (hP : MeasureTheory.IsProjectiveMeasureFamily P),
  (MeasureTheory.projectiveFamilyContent hP) s = MeasureTheory.projectiveFamilyFun P s
-- Mathlib.Analysis.Normed.Group.Basic
/-- **Triangle inequality** for the norm.  -/
norm_add₄_le : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] {a b c d : E}, ‖a + b + c + d‖ ≤ ‖a‖ + ‖b‖ + ‖c‖ + ‖d‖
-- Lean.Parser.Term
Lean.Parser.Term.completion.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskerRight_id : ∀ {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] {G : CategoryTheory.Functor C D}
  (F : CategoryTheory.Functor D E),
  CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.id G) F = CategoryTheory.NatTrans.id (G.comp F)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- Given a point in an affine subspace, a vector is in its direction if and only if it results from
subtracting that point on the left.  -/
AffineSubspace.mem_direction_iff_eq_vsub_left : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : AffineSubspace k P} {p : P}, p ∈ s → ∀ (v : V), v ∈ s.direction ↔ ∃ p₂ ∈ s, v = p -ᵥ p₂
-- Mathlib.Algebra.DirectSum.Decomposition
/-- A substructure `p ⊆ M` is homogeneous if for every `m ∈ p`, all homogeneous components
of `m` are in `p`.  -/
DirectSum.SetLike.IsHomogeneous : {ι : Type u_1} →
  {M : Type u_3} →
    {σ : Type u_4} →
      [inst : DecidableEq ι] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : SetLike σ M] →
            [inst_3 : AddSubmonoidClass σ M] →
              (ℳ : ι → σ) → [DirectSum.Decomposition ℳ] → {P : Type u_5} → [SetLike P M] → P → Prop
-- Mathlib.Algebra.Algebra.Subalgebra.Rank
Subalgebra.finrank_right_dvd_finrank_sup_of_free : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (A B : Subalgebra R S)
  [Module.Free R ↥B] [Module.Free ↥B ↥(Algebra.adjoin ↥B ↑A)], Module.finrank R ↥B ∣ Module.finrank R ↥(A ⊔ B)
-- Mathlib.Data.FunLike.Graded
/-- A graded map descends to a map on each component.  -/
Graded.subtypeMap : {F : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      {σ : Type u_4} →
        {τ : Type u_5} →
          {ι : Type u_6} →
            [inst : SetLike σ A] →
              [inst_1 : SetLike τ B] →
                {𝒜 : ι → σ} →
                  {ℬ : ι → τ} → [inst_2 : FunLike F A B] → [GradedFunLike F 𝒜 ℬ] → F → (i : ι) → ↥(𝒜 i) → ↥(ℬ i)
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
/-- For a manifold `M` and a smooth homomorphism `φ` between abelian Lie groups `A`, `A'`, the
'left-composition-by-`φ`' morphism of sheaves from `smoothSheafCommGroup IM I M A` to
`smoothSheafCommGroup IM I' M A'`.  -/
smoothSheafCommGroup.compLeft : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {EM : Type u_2} →
      [inst_1 : NormedAddCommGroup EM] →
        [inst_2 : NormedSpace 𝕜 EM] →
          {HM : Type u_3} →
            [inst_3 : TopologicalSpace HM] →
              (IM : ModelWithCorners 𝕜 EM HM) →
                {E : Type u_4} →
                  [inst_4 : NormedAddCommGroup E] →
                    [inst_5 : NormedSpace 𝕜 E] →
                      {H : Type u_5} →
                        [inst_6 : TopologicalSpace H] →
                          (I : ModelWithCorners 𝕜 E H) →
                            {H' : Type u_6} →
                              [inst_7 : TopologicalSpace H'] →
                                (I' : ModelWithCorners 𝕜 E H') →
                                  (M : Type u) →
                                    [inst_8 : TopologicalSpace M] →
                                      [inst_9 : ChartedSpace HM M] →
                                        (A A' : Type u) →
                                          [inst_10 : TopologicalSpace A] →
                                            [inst_11 : ChartedSpace H A] →
                                              [inst_12 : TopologicalSpace A'] →
                                                [inst_13 : ChartedSpace H' A'] →
                                                  [inst_14 : CommGroup A] →
                                                    [inst_15 : CommGroup A'] →
                                                      [inst_16 : LieGroup I (↑⊤) A] →
                                                        [inst_17 : LieGroup I' (↑⊤) A'] →
                                                          (φ : A →* A') →
                                                            ContMDiff I I' ↑⊤ ⇑φ →
                                                              (smoothSheafCommGroup IM I M A ⟶
                                                                smoothSheafCommGroup IM I' M A')
-- Mathlib.Algebra.Group.Prod
Prod.instSubsingletonUnits : ∀ {M : Type u_3} {N : Type u_4} [inst : Monoid M] [inst_1 : Monoid N] [Subsingleton Mˣ] [Subsingleton Nˣ],
  Subsingleton (M × N)ˣ
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.coe_sub_linearMap : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  (D1 D2 : LieDerivation R L M), ↑(D1 - D2) = ↑D1 - ↑D2
-- Init.Data.UInt.Lemmas
UInt32.ofBitVec_mod : ∀ (a b : BitVec 32), { toBitVec := a % b } = { toBitVec := a } % { toBitVec := b }
-- Aesop.Rule.Basic
Aesop.instInhabitedRule.default : {α : Type} → [Inhabited α] → Aesop.Rule α
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey?_inter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, (m₁ ∩ m₂).getKey? k = if k ∈ m₂ then m₁.getKey? k else none
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.mono_lift_of_mono_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {W X Y : C} (f : W ⟶ X) (g : W ⟶ Y) [CategoryTheory.Mono g],
  CategoryTheory.Mono (CategoryTheory.CartesianMonoidalCategory.lift f g)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.decorator.sizeOf_spec : sizeOf Lean.Lsp.SemanticTokenType.decorator = 1
-- Mathlib.GroupTheory.Coset.Basic
Subgroup.rightCosetEquivSubgroup.eq_1 : ∀ {α : Type u_1} [inst : Group α] {s : Subgroup α} (g : α),
  Subgroup.rightCosetEquivSubgroup g =
    { toFun := fun x => ⟨↑x * g⁻¹, ⋯⟩, invFun := fun x => ⟨↑x * g, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
-- Init.Data.List.TakeDrop
List.takeWhile_cons_of_pos : ∀ {α : Type u_1} {p : α → Bool} {a : α} {l : List α}, p a = true → List.takeWhile p (a :: l) = a :: List.takeWhile p l
-- Lean.Expr
Lean.Expr.const.injEq : ∀ (declName : Lean.Name) (us : List Lean.Level) (declName_1 : Lean.Name) (us_1 : List Lean.Level),
  (Lean.Expr.const declName us = Lean.Expr.const declName_1 us_1) = (declName = declName_1 ∧ us = us_1)
-- Init.Data.Array.Lemmas
Array.getElem_setIfInBounds : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} {a : α} {j : ℕ} (hj : j < xs.size),
  (xs.setIfInBounds i a)[j] = if i = j then a else xs[j]
-- Mathlib.Combinatorics.SimpleGraph.Clique
/-- If a set of vertices `A` is a clique in subgraph of `G` induced by a superset of `A`,
its embedding is a clique in `G`.  -/
SimpleGraph.IsClique.of_induce : ∀ {α : Type u_1} {G : SimpleGraph α} {S : G.Subgraph} {F : Set α} {A : Set ↑F},
  (S.induce F).coe.IsClique A → G.IsClique (Subtype.val '' A)
-- Mathlib.Algebra.Order.Monoid.Prod
Prod.instExistsAddOfLE : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] [inst_2 : Add α] [inst_3 : Add β] [ExistsAddOfLE α]
  [ExistsAddOfLE β], ExistsAddOfLE (α × β)
-- Mathlib.LinearAlgebra.ExteriorPower.Pairing
/-- The linear map from the exterior power of the dual to the dual of the exterior power.  -/
exteriorPower.pairingDual : (R : Type u_1) →
  (M : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → (n : ℕ) → ↥(⋀[R]^n (Module.Dual R M)) →ₗ[R] Module.Dual R ↥(⋀[R]^n M)
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
/-- **Alias** of `Order.cof_eq`. -/
Ordinal.cof_eq : ∀ (α : Type u) [inst : Preorder α], ∃ s, IsCofinal s ∧ Cardinal.mk ↑s = Order.cof α
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get_modify : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β) (h : (↑m).WF) {k k' : α} {f : β → β}
  (hc : (Std.DHashMap.Internal.Raw₀.Const.modify m k f).contains k' = true),
  Std.DHashMap.Internal.Raw₀.Const.get (Std.DHashMap.Internal.Raw₀.Const.modify m k f) k' hc =
    if heq : (k == k') = true then f (Std.DHashMap.Internal.Raw₀.Const.get m k ⋯)
    else Std.DHashMap.Internal.Raw₀.Const.get m k' ⋯
-- Mathlib.LinearAlgebra.Matrix.Basis
basis_toMatrix_basisFun_mul : ∀ {ι : Type u_1} {R : Type u_5} [inst : CommSemiring R] [inst_1 : Fintype ι] (b : Module.Basis ι R (ι → R))
  (A : Matrix ι ι R), b.toMatrix ⇑(Pi.basisFun R ι) * A = Matrix.of fun i j => (b.repr (A.col j)) i
-- Mathlib.CategoryTheory.Limits.Preserves.Filtered
/-- `ReflectsCofilteredLimitsOfSize.{w', w} F` means that whenever the image of a cofiltered cone
under `F` is a limit cone, the original cone was already a limit.  -/
CategoryTheory.Limits.ReflectsCofilteredLimitsOfSize : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → Prop
-- Mathlib.Algebra.Group.Opposite
SemiconjBy.op : ∀ {α : Type u_1} [inst : Mul α] {a x y : α},
  SemiconjBy a x y → SemiconjBy (MulOpposite.op a) (MulOpposite.op y) (MulOpposite.op x)