mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Algebra.Unitization
/-- this lemma establishes that if `ContinuousLinearMap.mul 𝕜 A` is injective, then so is
`Unitization.splitMul 𝕜 A`. When `A` is a `RegularNormedAlgebra`, then
`ContinuousLinearMap.mul 𝕜 A` is an isometry, and is therefore automatically injective.  -/
Unitization.splitMul_injective_of_clm_mul_injective : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : IsScalarTower 𝕜 A A] [inst_4 : SMulCommClass 𝕜 A A],
  Function.Injective ⇑(ContinuousLinearMap.mul 𝕜 A) → Function.Injective ⇑(Unitization.splitMul 𝕜 A)
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
/-- The preferred extended chart on a manifold with corners around a point `x`, from a neighborhood
of `x` to the model vector space.  -/
extChartAt : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {M : Type u_3} →
      {H : Type u_4} →
        [inst : NontriviallyNormedField 𝕜] →
          [inst_1 : NormedAddCommGroup E] →
            [inst_2 : NormedSpace 𝕜 E] →
              [inst_3 : TopologicalSpace H] →
                [inst_4 : TopologicalSpace M] → ModelWithCorners 𝕜 E H → [ChartedSpace H M] → M → PartialEquiv M E
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.diffₘ.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β),
  m₁.diffₘ m₂ =
    if (↑m₁).size ≤ (↑m₂).size then m₁.filterₘ fun k x => !m₂.containsₘ k
    else ↑(m₁.eraseManyEntries (Std.DHashMap.Internal.toListModel (↑m₂).buckets))
-- Mathlib.Algebra.Module.Submodule.Ker
LinearMap.ker_toAddSubmonoid : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  (f : M →ₛₗ[τ₁₂] M₂), f.ker.toAddSubmonoid = AddMonoidHom.mker f
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalCategory.tensor_associativity : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategory.tensorμ X₁ X₂ Y₁ Y₂)
        (CategoryTheory.MonoidalCategoryStruct.tensorObj Z₁ Z₂))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.tensorμ (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ Y₁)
          (CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ Y₂) Z₁ Z₂)
        (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.associator X₁ Y₁ Z₁).hom
          (CategoryTheory.MonoidalCategoryStruct.associator X₂ Y₂ Z₂).hom)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂)
          (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₁ Y₂)
          (CategoryTheory.MonoidalCategoryStruct.tensorObj Z₁ Z₂)).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂)
          (CategoryTheory.MonoidalCategory.tensorμ Y₁ Y₂ Z₁ Z₂))
        (CategoryTheory.MonoidalCategory.tensorμ X₁ X₂ (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₁ Z₁)
          (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₂ Z₂)))
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.mk.sizeOf_spec : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B]
  [inst_4 : SMul R A] [inst_5 : SMul R B] [inst_6 : Star A] [inst_7 : Star B] [inst_8 : SizeOf R] [inst_9 : SizeOf A]
  [inst_10 : SizeOf B] (toStarRingEquiv : A ≃⋆+* B)
  (map_smul' : ∀ (r : R) (a : A), toStarRingEquiv.toFun (r • a) = r • toStarRingEquiv.toFun a),
  sizeOf { toStarRingEquiv := toStarRingEquiv, map_smul' := map_smul' } = 1 + sizeOf toStarRingEquiv
-- Mathlib.Algebra.Category.ModuleCat.Basic
_private.Mathlib.Algebra.Category.ModuleCat.Basic.0.ModuleCat.mk.sizeOf_spec : ∀ {R : Type u} [inst : Ring R] [inst_1 : SizeOf R] (carrier : Type v) [isAddCommGroup : AddCommGroup carrier]
  [isModule : Module R carrier],
  sizeOf { carrier := carrier, isAddCommGroup := isAddCommGroup, isModule := isModule } =
    1 + sizeOf carrier + sizeOf isAddCommGroup + sizeOf isModule
-- Mathlib.RingTheory.Spectrum.Maximal.Basic
MaximalSpectrum.instNonemptyOfNontrivial : ∀ {R : Type u_1} [inst : CommSemiring R] [Nontrivial R], Nonempty (MaximalSpectrum R)
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.germ_stalkPullbackHom_assoc : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X Y : TopCat}
  (f : X ⟶ Y) (F : TopCat.Presheaf C Y) (x : ↑X) (U : TopologicalSpace.Opens ↑Y)
  (hU : (CategoryTheory.ConcreteCategory.hom f) x ∈ U) {Z : C} (h : ((TopCat.Presheaf.pullback C f).obj F).stalk x ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.germ U ((CategoryTheory.ConcreteCategory.hom f) x) hU)
      (CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.stalkPullbackHom C f F x) h) =
    CategoryTheory.CategoryStruct.comp
      (((TopCat.Presheaf.pullbackPushforwardAdjunction C f).unit.app F).app (Opposite.op U))
      (CategoryTheory.CategoryStruct.comp
        (((TopCat.Presheaf.pullback C f).obj F).germ ((TopologicalSpace.Opens.map f).obj U) x hU) h)
-- Mathlib.Topology.Separation.Basic
specializes_eq_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X], (fun x1 x2 => x1 ⤳ x2) = Eq
-- Init.Internal.Order.Basic
Lean.Order.FlatOrder.rel.bot : ∀ {α : Sort u} {b : α} {x : Lean.Order.FlatOrder b}, Lean.Order.FlatOrder.rel b x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PushoutObjObj.inr_ι_assoc : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂}
  (self : F.PushoutObjObj f₁ f₂) {Z : C₃} (h : (F.obj Y₁).obj Y₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.inr (CategoryTheory.CategoryStruct.comp self.ι h) =
    CategoryTheory.CategoryStruct.comp ((F.map f₁).app Y₂) h
-- Mathlib.Order.Heyting.Hom
/-- `CoheytingHomClass F α β` states that `F` is a type of co-Heyting homomorphisms.

You should extend this class when you extend `CoheytingHom`.  -/
CoheytingHomClass : (F : Type u_6) → (α : Type u_7) → (β : Type u_8) → [CoheytingAlgebra α] → [CoheytingAlgebra β] → [FunLike F α β] → Prop
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.setIntegral_dirac' : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {f : X → E} [inst_3 : NormedSpace ℝ E]
  [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} {mX : MeasurableSpace X}
  [CompleteSpace G] {a : X} {v : F},
  MeasureTheory.StronglyMeasurable f →
    ∀ {s : Set X},
      MeasurableSet s →
        ∀ [inst_7 : Decidable (a ∈ s)],
          ∫ᵛ (x : X) in s, f x ∂[B; MeasureTheory.VectorMeasure.dirac a v] = if a ∈ s then (B (f a)) v else 0
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.prod_rpow_of_ne_top : ∀ {ι : Type u_1} {s : Finset ι} {f : ι → ENNReal}, (∀ i ∈ s, f i ≠ ⊤) → ∀ (r : ℝ), ∏ i ∈ s, f i ^ r = (∏ i ∈ s, f i) ^ r
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.cos_sin_inj : ∀ {θ ψ : ℝ}, Real.cos θ = Real.cos ψ → Real.sin θ = Real.sin ψ → ↑θ = ↑ψ
-- Mathlib.Data.List.Sort
List.Subset.antisymm_of_sortedGT : ∀ {α : Type u_1} [inst : PartialOrder α] {l₁ l₂ : List α}, l₁ ⊆ l₂ → l₂ ⊆ l₁ → l₁.SortedGT → l₂.SortedGT → l₁ = l₂
-- Mathlib.Data.Finset.Update
Function.updateFinset.eq_1 : ∀ {ι : Type u_1} {π : ι → Sort u_2} [inst : DecidableEq ι] (x : (i : ι) → π i) (s : Finset ι) (y : (i : ↥s) → π ↑i)
  (i : ι), Function.updateFinset x s y i = if hi : i ∈ s then y ⟨i, hi⟩ else x i
-- Init.Data.String.Decode
UInt8.instDecidableIsUTF8FirstByte : {c : UInt8} → Decidable c.IsUTF8FirstByte
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasurableEquiv.smul.eq_1 : ∀ {G : Type u_1} {α : Type u_3} [inst : MeasurableSpace α] [inst_1 : Group G] [inst_2 : MulAction G α]
  [inst_3 : MeasurableConstSMul G α] (c : G),
  MeasurableEquiv.smul c = { toEquiv := MulAction.toPerm c, measurable_toFun := ⋯, measurable_invFun := ⋯ }
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.ext : ∀ {α : Type u_4} {x y : Hypergraph α}, x.vertexSet = y.vertexSet → x.edgeSet = y.edgeSet → x = y
-- Mathlib.Data.Multiset.Defs
Multiset.instHasSSubset : {α : Type u_1} → HasSSubset (Multiset α)
-- Std.Internal.Do.Order.Basic
Lean.Order.iInf_le : ∀ {α : Type u} [inst : Lean.Order.CompleteLattice α] {ι : Type v} (f : ι → α) (i : ι),
  Lean.Order.PartialOrder.rel (Lean.Order.iInf f) (f i)
-- Init.Data.Fin.Lemmas
Fin.lastCases_last : ∀ {n : ℕ} {motive : Fin (n + 1) → Sort u_1} {last : motive (Fin.last n)} {cast : (i : Fin n) → motive i.castSucc},
  Fin.lastCases last cast (Fin.last n) = last
-- Lean.Meta.LitValues
/-- If `e` is a `Nat`, `Int`, or `Fin` literal value, converts it into a constructor application.
Otherwise, just return `e`.
 -/
Lean.Meta.litToCtor : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Group.Action.Hom
MonoidHom.smulOneHom_apply : ∀ {M : Type u_4} {N : Type u_5} [inst : Monoid M] [inst_1 : MulOneClass N] [inst_2 : MulAction M N]
  [inst_3 : IsScalarTower M N N] (x : M), MonoidHom.smulOneHom x = x • 1
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.below.add_assoc : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  {motive : (a a_1 : CommRingCat.Colimits.Prequotient F) → CommRingCat.Colimits.Relation F a a_1 → Prop}
  (x y z : CommRingCat.Colimits.Prequotient F), CommRingCat.Colimits.Relation.below ⋯
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.tendsto_nhds_of_Icc : ∀ {α : Type u_1} {f : Filter α} {u : α → ENNReal} {a : ENNReal},
  (∀ ε > 0, ∀ᶠ (x : α) in f, u x ∈ Set.Icc (a - ε) (a + ε)) → Filter.Tendsto u f (nhds a)
-- Mathlib.Logic.Relator
Relator.BiTotal.refl : ∀ {α : Type u_1} {r₁₁ : α → α → Prop}, (∀ (a : α), r₁₁ a a) → Relator.BiTotal r₁₁
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.toCLM_sub : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] [inst_8 : IsTopologicalAddGroup F]
  {f g : E →SWOT[σ] F}, (f - g).toCLM = f.toCLM - g.toCLM
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsNeg.eq_1 : ∀ (m : Tactic.ComputeAsymptotics.UnitMonomial),
  m.FirstNonzeroIsNeg = (m.sign = Tactic.ComputeAsymptotics.UnitMonomial.Sign.neg)
-- Lean.Elab.App
Lean.Elab.Term.LValResolution.const.inj : ∀ {baseStructName structName constName : Lean.Name} {levels : List Lean.Level}
  {baseStructName_1 structName_1 constName_1 : Lean.Name} {levels_1 : List Lean.Level},
  Lean.Elab.Term.LValResolution.const baseStructName structName constName levels =
      Lean.Elab.Term.LValResolution.const baseStructName_1 structName_1 constName_1 levels_1 →
    baseStructName = baseStructName_1 ∧ structName = structName_1 ∧ constName = constName_1 ∧ levels = levels_1
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.isEmpty_modify : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp},
  t.WF → ∀ {k : α} {f : β → β}, (Std.DTreeMap.Raw.Const.modify t k f).isEmpty = t.isEmpty
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.apply_eq_of_isPreconnected : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] (f : LocallyConstant X Y) {s : Set X},
  IsPreconnected s → ∀ {x y : X}, x ∈ s → y ∈ s → f x = f y
-- Lean.Language.Basic
/-- A task producing some snapshot type (usually a subclass of `Snapshot`).  -/
Lean.Language.SnapshotTask : Type → Type
-- Aesop.Search.Expansion.Norm
Aesop.optNormRuleResultToNormSeqResult : Option (Aesop.DisplayRuleName × Aesop.NormRuleResult) → Aesop.NormSeqResult
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- Equality of the composition of the unit, associator, and counit with the identity
`G ⟶ G (F G) ⟶ (F G) F ⟶ G = NatTrans.id G`  -/
CategoryTheory.Adjunction.CoreUnitCounit.right_triangle : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (self : CategoryTheory.Adjunction.CoreUnitCounit F G),
  CategoryTheory.CategoryStruct.comp (G.whiskerLeft self.unit)
      (CategoryTheory.CategoryStruct.comp (G.associator F G).inv (CategoryTheory.Functor.whiskerRight self.counit G)) =
    CategoryTheory.NatTrans.id (G.comp (CategoryTheory.Functor.id C))
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.toCompacts_singleton : ∀ {α : Type u_1} [inst : TopologicalSpace α] (x : α), {x}.toCompacts = {x}
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.abs_sin_eq_of_two_zsmul_eq : ∀ {θ ψ : Real.Angle}, 2 • θ = 2 • ψ → |θ.sin| = |ψ.sin|
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubMulAction.ofFixingSubgroup_carrier : ∀ (M : Type u_1) {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] (s : Set α),
  (SubMulAction.ofFixingSubgroup M s).carrier = sᶜ
-- Mathlib.Topology.Category.TopCat.Adjunctions
TopCat.adj₂_counit : TopCat.adj₂.counit = CategoryTheory.CategoryStruct.id (TopCat.trivial.comp (CategoryTheory.forget TopCat))
-- Mathlib.RingTheory.LinearDisjoint
Subalgebra.LinearDisjoint.eq_bot_of_self : ∀ {R : Type u} {S : Type v} [inst : Field R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {A : Subalgebra R S},
  A.LinearDisjoint A → A = ⊥
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.rightHom_surjective : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {φ : G →* MulAut N},
  Function.Surjective ⇑SemidirectProduct.rightHom
-- Mathlib.Probability.Process.Predictable
MeasureTheory.measurableSet_predictable_singleton_bot_prod : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : LinearOrder ι] [inst_1 : OrderBot ι]
  {𝓕 : MeasureTheory.Filtration ι m} {s : Set Ω}, MeasurableSet s → MeasurableSet ({⊥} ×ˢ s)
-- Init.Data.SInt.Basic
/-- Non-strict inequality of 32-bit signed integers, defined as inequality of the corresponding integers.
Usually accessed via the `≤` operator.
 -/
Int32.le : Int32 → Int32 → Prop
-- Mathlib.Data.List.Defs
_private.Mathlib.Data.List.Defs.0.List.headI.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (tail : List α) → motive (a :: tail)),
  (match [] with
    | [] => h_1 ()
    | a :: tail => h_2 a tail) =
    h_1 ()
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.instIsSMulApply : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} {R : Type u_5} [inst_4 : Semiring R]
  [inst_5 : Module R F] [inst_6 : SMulCommClass ℝ R F] [inst_7 : ContinuousConstSMul R F],
  IsSMulApply R (ContDiffMapSupportedIn E F n K) E F
-- Mathlib.Geometry.Euclidean.MongePoint
Affine.Simplex.mongePlane_reindex : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {m n : ℕ} (s : Affine.Simplex ℝ P (n + 2)) (e : Fin (n + 3) ≃ Fin (m + 3))
  (i₁ i₂ : Fin (m + 3)), (s.reindex e).mongePlane i₁ i₂ = s.mongePlane (e.symm i₁) (e.symm i₂)
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.fst'_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y Z X : C} (f : Y ⟶ X) (g : Z ⟶ X)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong g],
  CategoryTheory.Over.Hom.left (CategoryTheory.ChosenPullbacksAlong.fst' f g) =
    CategoryTheory.ChosenPullbacksAlong.fst f g
-- Mathlib.RingTheory.Idempotents
OrthogonalIdempotents.map : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) {I : Type u_3} {e : I → R},
  OrthogonalIdempotents e → OrthogonalIdempotents (⇑f ∘ e)
-- Mathlib.CategoryTheory.Preadditive.Projective.Resolution
/-- Given projective resolutions `P` and `P'` of two objects `Z` and `Z'`,
and a morphism `f : Z ⟶ Z'`, this structure contains the data of a morphism
`P.complex ⟶ P'.complex` which is compatible with `f`  -/
CategoryTheory.ProjectiveResolution.Hom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {Z : C} →
          CategoryTheory.ProjectiveResolution Z → {Z' : C} → CategoryTheory.ProjectiveResolution Z' → (Z ⟶ Z') → Type v
-- Mathlib.CategoryTheory.Sums.Basic
CategoryTheory.Sum.swap_obj_inl : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : C), (CategoryTheory.Sum.swap C D).obj (Sum.inl X) = Sum.inr X
-- Mathlib.CategoryTheory.GradedObject
/-- Given `X : GradedObject I C` and `p : I → J`, `X.mapObj p` is the graded object by `J`
which in degree `j` consists of the coproduct of the `X i` such that `p i = j`.  -/
CategoryTheory.GradedObject.mapObj : {I : Type u_1} →
  {J : Type u_2} →
    {C : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_4} C] →
        (X : CategoryTheory.GradedObject I C) → (p : I → J) → [X.HasMap p] → CategoryTheory.GradedObject J C
-- Mathlib.Topology.Algebra.Module.Equiv
/-- Continuous linear equivalences between modules. We only put the type classes that are necessary
for the definition, although in applications `M` and `M₂` will be topological modules over the
topological semiring `R`.  -/
«term_≃SL[_]_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Category.Bipointed
Bipointed.mk.sizeOf_spec : ∀ (X : Type u) (toProd : X × X), sizeOf { X := X, toProd := toProd } = 1 + sizeOf X + sizeOf toProd
-- Mathlib.Tactic.GCongr.Core
/-- Apply generalized congruence lemma `lem` to goal `g`, throwing an error if it fails.
Return an array of main subgoals and an array of side goals.
For each main subgoal, also return whether the sides of the relation are swapped
(i.e. whether it is contravariant).

This function is used by both the `gcongr` and `grw` tactic.
In the case of `grw`, one of the two sides of the goal is a metavariable that is filled in
by this function.

In the main subgoals, the forall binders are introduced. They are named using the `with` clause of
`gcongr`, or otherwise using binder names in the goal. `grw` relies on these names to ensure that
binder names are preserved in the goal.
 -/
Mathlib.Tactic.GCongr.applyGCongrLemma : Lean.MVarId →
  Mathlib.Tactic.GCongr.GCongrLemma → Mathlib.Tactic.GCongr.GCongrM (Array (Lean.MVarId × Bool) × Array Lean.MVarId)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
CategoryTheory.Limits.hasPullback_assoc_symm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁)
  (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [inst_1 : CategoryTheory.Limits.HasPullback f₁ f₂]
  [inst_2 : CategoryTheory.Limits.HasPullback f₃ f₄]
  [CategoryTheory.Limits.HasPullback f₁
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)],
  CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃)
    f₄
-- Mathlib.Order.Defs.PartialOrder
le_antisymm : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = b
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey!_eq_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.isEmpty = false → ∀ {km : α}, t.minKey! = km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Std.Time.Format.Basic
/-- Classify a `PlainTime` into a `DayPeriod` for the `b` pattern.  -/
Std.Time.classifyDayPeriod : Std.Time.Hour.Ordinal → Std.Time.Minute.Ordinal → Std.Time.Second.Ordinal true → Std.Time.DayPeriod
-- Mathlib.Topology.Maps.Basic
IsOpenMap.clusterPt_comap : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  IsOpenMap f → ∀ {x : X} {l : Filter Y}, ClusterPt (f x) l → ClusterPt x (Filter.comap f l)
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
IsSymmetricAlgebra.lift.congr_simp : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_3}
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] {f f_1 : M →ₗ[R] A} (e_f : f = f_1) (h : IsSymmetricAlgebra f)
  {A' : Type u_4} [inst_5 : CommSemiring A'] [inst_6 : Algebra R A'] (g g_1 : M →ₗ[R] A'),
  g = g_1 → h.lift g = ⋯.lift g_1
-- Mathlib.Order.Bounds.Basic
IsLUB.mono : ∀ {α : Type u_1} [inst : Preorder α] {s t : Set α} {a b : α}, IsLUB s a → IsLUB t b → s ⊆ t → a ≤ b
-- Mathlib.Data.Set.Insert
Set.insert_subset_insert : ∀ {α : Type u_1} {s t : Set α} {a : α}, s ⊆ t → insert a s ⊆ insert a t
-- Mathlib.Algebra.Category.Grp.Yoneda
AddCommGrpCat.coyonedaType.eq_1 : AddCommGrpCat.coyonedaType =
  {
    obj := fun X =>
      { obj := fun G => AddCommGrpCat.of (Opposite.unop X → ↑G),
        map := fun {X_1 Y} f =>
          AddCommGrpCat.ofHom
            (AddMonoidHom.pi fun i => (AddCommGrpCat.Hom.hom f).comp (Pi.evalAddMonoidHom (fun a => ↑X_1) i)),
        map_id := ⋯, map_comp := ⋯ },
    map := fun {X Y} f =>
      {
        app := fun G =>
          AddCommGrpCat.ofHom
            (AddMonoidHom.pi fun i =>
              Pi.evalAddMonoidHom (fun a => ↑G) ((CategoryTheory.ConcreteCategory.hom f.unop) i)),
        naturality := ⋯ },
    map_id := AddCommGrpCat.coyonedaType._proof_4, map_comp := @AddCommGrpCat.coyonedaType._proof_5 }
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cocycle.homOf_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (z : CochainComplex.HomComplex.Cocycle F G 0) (i : ℤ), z.homOf.f i = (↑z).v i i ⋯
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
ContinuousMapZero.continuous_toNNReal : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : Zero X], Continuous ContinuousMapZero.toNNReal
-- Mathlib.Analysis.SpecialFunctions.Artanh
Real.strictMonoOn_one_add_div_one_sub : StrictMonoOn (fun x => (1 + x) / (1 - x)) (Set.Ioo (-1) 1)
-- Mathlib.RingTheory.Coalgebra.MonoidAlgebra
LaurentPolynomial.comul_C_mul_T_self : ∀ {R : Type u_1} [inst : CommSemiring R] (a : R) (n : ℤ),
  CoalgebraStruct.comul (LaurentPolynomial.C a * LaurentPolynomial.T n) =
    LaurentPolynomial.T n ⊗ₜ[R] (LaurentPolynomial.C a * LaurentPolynomial.T n)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SavedState.mk.inj : ∀ {«meta» : Lean.Meta.SavedState} {grind : Lean.Meta.Grind.State} {meta_1 : Lean.Meta.SavedState}
  {grind_1 : Lean.Meta.Grind.State},
  { «meta» := «meta», grind := grind } = { «meta» := meta_1, grind := grind_1 } → «meta» = meta_1 ∧ grind = grind_1
-- Mathlib.Topology.MetricSpace.Basic
instMetricSpaceULift : {β : Type v} → [MetricSpace β] → MetricSpace (ULift.{u_2, v} β)
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsAddFundamentalDomain.measure_addFundamentalInterior : ∀ {G : Type u_1} {α : Type u_3} [Countable G] [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α]
  {μ : MeasureTheory.Measure α} {s : Set α},
  MeasureTheory.IsAddFundamentalDomain G s μ → μ (MeasureTheory.addFundamentalInterior G s) = μ s