mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- The induced algebras morphism from the quotient by the kernel to the codomain.

This is an isomorphism if `f` has a right inverse (`quotientKerAlgEquivOfRightInverse`) /
is surjective (`quotientKerAlgEquivOfSurjective`).
 -/
Ideal.kerLiftAlg : {R₁ : Type u_1} →
  {A : Type u_3} →
    {B : Type u_4} →
      [inst : CommSemiring R₁] →
        [inst_1 : Ring A] →
          [inst_2 : Algebra R₁ A] →
            [inst_3 : Semiring B] → [inst_4 : Algebra R₁ B] → (f : A →ₐ[R₁] B) → A ⧸ RingHom.ker f →ₐ[R₁] B
-- Mathlib.RingTheory.OrderOfVanishing.Noetherian
/-- For `x y : R`, if `x + y ≠ 0` then `min (ordFrac R x) (ordFrac R y) ≤ ordFrac R (x + y)`. The
condition that `x + y ≠ 0` is used to guarantee that all the elements we're taking `ordFrac` of
are nonzero, meaning none of them will be `0` in `ℤᵐ⁰`. This allows us to use `ord_add` (which
uses the ordering on `ℕ∞`), since these orders correspond on non `⊤` elements.
 -/
Ring.ordFrac_add : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra R K] [inst_5 : IsFractionRing R K] (x y : K),
  x + y ≠ 0 → min ((Ring.ordFrac R) x) ((Ring.ordFrac R) y) ≤ (Ring.ordFrac R) (x + y)
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.coeSubmoduleHom_apply : ∀ {R : Type u_1} [inst : CommRing R] (S : Submonoid R) (P : Type u_2) [inst_1 : CommRing P] [inst_2 : Algebra R P]
  (I : FractionalIdeal S P), (FractionalIdeal.coeSubmoduleHom S P) I = ↑I
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.map_id : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] (S : L.Substructure M),
  FirstOrder.Language.Substructure.map (FirstOrder.Language.Hom.id L M) S = S
-- Mathlib.Data.Finset.Max
Finset.isGreatest_max' : ∀ {α : Type u_2} [inst : LinearOrder α] (s : Finset α) (H : s.Nonempty), IsGreatest (↑s) (s.max' H)
-- Lean.Elab.SetOption
Lean.Elab.validateOptionValue : {m : Type → Type} → [Monad m] → [Lean.MonadError m] → Lean.Name → Lean.OptionDecl → Lean.DataValue → m Unit
-- Lean.Meta.Tactic.Simp.SimpTheorems
/-- Like `isRflProof`, but also returns `true` for proofs that are rfl only at default
transparency (via `@[backward_defeq]`).  -/
Lean.Meta.isBackwardRflProof : Lean.Expr → Lean.MetaM Bool
-- Init.Data.Bool
Bool.cond_eq_true_distrib : ∀ (c t f : Bool), ((bif c then t else f) = true) = if c = true then t = true else f = true
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
RingEquiv.mapTwoSidedIdeal_symm : ∀ {R : Type u_1} {S : Type u_2} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S] (e : R ≃+* S),
  e.mapTwoSidedIdeal.symm = e.symm.mapTwoSidedIdeal
-- Mathlib.RingTheory.Coprime.Basic
IsRelPrime.sub_mul_right_left_iff : ∀ {R : Type u_1} [inst : CommRing R] {x y z : R}, IsRelPrime (x - z * y) y ↔ IsRelPrime x y
-- Mathlib.Topology.ShrinkingLemma
/-- **Shrinking lemma**. A point-finite open cover of a compact subset of a locally compact T2 space
can be "shrunk" to a new closed cover so that each new closed set is contained in the corresponding
original open set. See also `exists_subset_iUnion_closure_subset_t2space` for a stronger statement.
 -/
exists_subset_iUnion_compact_subset_t2space : ∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {u : ι → Set X} {s : Set X} [T2Space X]
  [LocallyCompactSpace X],
  IsCompact s →
    (∀ (i : ι), IsOpen (u i)) →
      (∀ x ∈ s, {i | x ∈ u i}.Finite) →
        s ⊆ ⋃ i, u i →
          ∃ v, s ⊆ Set.iUnion v ∧ (∀ (i : ι), IsClosed (v i)) ∧ (∀ (i : ι), v i ⊆ u i) ∧ ∀ (i : ι), IsCompact (v i)
-- Std.Data.Iterators.Lemmas.Producers.Repeat
Std.Iter.toList_take_repeat_succ : ∀ {α : Type w} {f : α → α} {init : α} {k : ℕ},
  (Std.Iter.take (k + 1) (Std.Iter.repeat f init)).toList =
    init :: (Std.Iter.take k (Std.Iter.repeat f (f init))).toList
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.le_weightedOrder_smul : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (w : σ → ℕ) {f : MvPowerSeries σ R} {a : R},
  MvPowerSeries.weightedOrder w f ≤ MvPowerSeries.weightedOrder w (a • f)
-- Mathlib.RingTheory.Localization.Module
span_eq_top_of_isLocalizedModule : ∀ {R : Type u_1} (Rₛ : Type u_2) [inst : CommSemiring R] (S : Submonoid R) [inst_1 : CommSemiring Rₛ]
  [inst_2 : Algebra R Rₛ] [IsLocalization S Rₛ] {M : Type u_3} {Mₛ : Type u_4} [inst_4 : AddCommMonoid M]
  [inst_5 : Module R M] [inst_6 : AddCommMonoid Mₛ] [inst_7 : Module R Mₛ] [inst_8 : Module Rₛ Mₛ]
  [IsScalarTower R Rₛ Mₛ] (f : M →ₗ[R] Mₛ) [IsLocalizedModule S f] {v : Set M},
  Submodule.span R v = ⊤ → Submodule.span Rₛ (⇑f '' v) = ⊤
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
SSet.PtSimplex.RelStruct.δ_map_of_lt : ∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex n x} {i : Fin (n + 1)}
  (self : f.RelStruct g i),
  ∀ j < i.castSucc, CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) self.map = SSet.const x
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.noConfusionType : Sort v✝ → Std.Tactic.BVDecide.LRAT.Internal.Assignment → Std.Tactic.BVDecide.LRAT.Internal.Assignment → Sort v✝
-- Mathlib.Data.Holor
Holor.mul_scalar_mul : ∀ {α : Type} {ds : List ℕ} [inst : Mul α] (x : Holor α []) (y : Holor α ds), x.mul y = x ⟨[], ⋯⟩ • y
-- Init.Data.UInt.IntToBitVec
USize.toBitVec32_shiftLeft : ∀ (a b : USize) (h : System.Platform.numBits = 32), (a <<< b).toBitVec32 h = a.toBitVec32 h <<< (b.toBitVec32 h % 32)
-- Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
/-- In the notation of the module docstring: Since `T` is standard smooth
of relative dimension one over `S`, `K/K²` is free of rank one generated
by the image of `g * X - 1`.
This is the section `K/K² → J/J²` defined by sending the image of `g * X - 1` to `x : J/J²`.
 -/
Algebra.Generators.cotangentCompAwaySec : {R : Type u_1} →
  {S : Type u_2} →
    {T : Type u_3} →
      {ι : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              [inst_3 : CommRing T] →
                [inst_4 : Algebra R T] →
                  [inst_5 : Algebra S T] →
                    [inst_6 : IsScalarTower R S T] →
                      (g : S) →
                        [inst_7 : IsLocalization.Away g T] →
                          (P : Algebra.Generators R S ι) →
                            ((Algebra.Generators.localizationAway T g).comp P).toExtension.Cotangent →
                              (Algebra.Generators.localizationAway T g).toExtension.Cotangent →ₗ[T]
                                ((Algebra.Generators.localizationAway T g).comp P).toExtension.Cotangent
-- Std.Data.DTreeMap.Basic
/-- Returns an array of all values present in the tree map in ascending  order.  -/
Std.DTreeMap.valuesArray : {α : Type u} → {cmp : α → α → Ordering} → {β : Type v} → Std.DTreeMap α (fun x => β) cmp → Array β
-- Lean.Elab.PreDefinition.TerminationHint
/-- The termination annotations for a single function.
For `decreasing_by`, we store the whole `decreasing_by tacticSeq` expression, as this
is what `Term.runTactic` expects.
  -/
Lean.Elab.TerminationHints : Type
-- Mathlib.Topology.Algebra.Group.Basic
/-- A version of `Homeomorph.mulLeft a b⁻¹` that is defeq to `a / b`.  -/
Homeomorph.divLeft : {G : Type w} → [inst : Group G] → [inst_1 : TopologicalSpace G] → [IsTopologicalGroup G] → G → G ≃ₜ G
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
DihedralGroup.sr.inj : ∀ {n : ℕ} {a a_1 : ZMod n}, DihedralGroup.sr a = DihedralGroup.sr a_1 → a = a_1
-- Lean.Meta.SynthInstance
/-- Target type has metavariables, and class does not have output parameters.  -/
_private.Lean.Meta.SynthInstance.0.Lean.Meta.PreprocessKind.mvarsNoOutputParams : Lean.Meta.PreprocessKind✝
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrix_one : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_4} [inst_1 : Fintype n] [inst_2 : DecidableEq n] {M₁ : Type u_5}
  [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M₁] (v₁ : Module.Basis n R M₁), (LinearMap.toMatrix v₁ v₁) 1 = 1
-- Mathlib.Logic.Function.Basic
Function.curry_update : ∀ {α : Type u_1} {α' : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq α'] (f : α × α' → β)
  (aa' : α × α') (b : β),
  Function.curry (Function.update f aa' b) =
    Function.update (Function.curry f) aa'.1 (Function.update (Function.curry f aa'.1) aa'.2 b)
-- Mathlib.Algebra.Group.Subgroup.Actions
/-- The center of a group acts commutatively on that group.  -/
Subgroup.center.smulCommClass_left : ∀ {G : Type u_1} [inst : Group G], SMulCommClass (↥(Subgroup.center G)) G G
-- Mathlib.Probability.Kernel.CondDistrib
ProbabilityTheory.condExp_ae_eq_integral_condDistrib_id : ∀ {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] [inst_3 : NormedAddCommGroup F] {mβ : MeasurableSpace β} [inst_4 : NormedSpace ℝ F]
  [CompleteSpace F] {X : Ω → β} {μ : MeasureTheory.Measure Ω} [inst_6 : MeasureTheory.IsFiniteMeasure μ],
  Measurable X →
    ∀ {f : Ω → F},
      MeasureTheory.Integrable f μ →
        μ[f | MeasurableSpace.comap X mβ] =ᵐ[μ] fun a => ∫ (y : Ω), f y ∂(ProbabilityTheory.condDistrib id X μ) (X a)
-- Mathlib.Tactic.CrossRefAttribute
Mathlib.CrossRef.instHashableTag : Hashable Mathlib.CrossRef.Tag
-- Mathlib.Combinatorics.SetFamily.Shadow
/-- `s ∈ ∂ 𝒜` iff `s` is exactly one element less than something from `𝒜`.

See also `Finset.mem_shadow_iff_exists_sdiff`.  -/
Finset.mem_shadow_iff_exists_mem_card_add_one : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {t : Finset α},
  t ∈ 𝒜.shadow ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ s.card = t.card + 1
-- Mathlib.SetTheory.Ordinal.Notation
/-- Auxiliary definition to compute the ordinal notation for the ordinal exponentiation in `opow`  -/
ONote.opowAux : ONote → ONote → ONote → ℕ → ℕ → ONote
-- Mathlib.Analysis.Convex.Side
AffineSubspace.isConnected_setOfPred_wSameSide : ∀ {V : Type u_2} {P : Type u_4} [inst : SeminormedAddCommGroup V] [inst_1 : NormedSpace ℝ V]
  [inst_2 : PseudoMetricSpace P] [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} (x : P),
  (↑s).Nonempty → IsConnected {y | s.WSameSide x y}
-- Mathlib.LinearAlgebra.FreeModule.PID
/-- Given a Smith-normal-form pair of bases for `N ⊆ M`, and a linear endomorphism `f` of `M`
that preserves `N`, the diagonal of the matrix of the restriction `f` to `N` does not depend on
which of the two bases for `N` is used.  -/
Module.Basis.SmithNormalForm.toMatrix_restrict_eq_toMatrix : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {n : ℕ} {N : Submodule R M} (snf : Module.Basis.SmithNormalForm N ι n) [inst_3 : Fintype ι] [inst_4 : DecidableEq ι]
  (f : M →ₗ[R] M) (hf : ∀ (x : M), f x ∈ N) (hf' : optParam (∀ x ∈ N, f x ∈ N) ⋯) {i : Fin n},
  (LinearMap.toMatrix snf.bN snf.bN) (f.restrict hf') i i = (LinearMap.toMatrix snf.bM snf.bM) f (snf.f i) (snf.f i)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k k' : α} {f : β k → β k} {hc : k' ∈ t.modify k f},
  (t.modify k f).get k' hc = if heq : cmp k k' = Ordering.eq then cast ⋯ (f (t.get k ⋯)) else t.get k' ⋯
-- Std.Time.DateTime.WallTime
Std.Time.WallTime.instHAddOffset_3 : HAdd Std.Time.WallTime Std.Time.Minute.Offset Std.Time.WallTime
-- Std.Data.Internal.List.Associative
Std.Internal.List.replaceEntry_of_perm : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l l' : List ((a : α) × β a)} {k : α} {v : β k},
  Std.Internal.List.DistinctKeys l →
    l.Perm l' → (Std.Internal.List.replaceEntry k v l).Perm (Std.Internal.List.replaceEntry k v l')
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
AddLECancellable.le_tsub_iff_right : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α}, AddLECancellable a → a ≤ c → (b ≤ c - a ↔ b + a ≤ c)
-- Mathlib.RingTheory.Valuation.Basic
Valuation.map_add_of_left_eq_zero : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀)
  {x y : R}, v x = 0 → v (x + y) = v y
-- Mathlib.Algebra.Group.End
/-- **Alias** of `AddAut.add_def`. -/
AddAut.mul_def : ∀ (M : Type u_2) [inst : Add M] (e₁ e₂ : AddAut M), e₁ + e₂ = AddEquiv.trans e₂ e₁
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.completeAtomicBooleanAlgebra : {V : Type u} → CompleteAtomicBooleanAlgebra (SimpleGraph V)
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnModule.of_symm_zero : ∀ {Γ : Type u_1} {R : Type u_3} {V : Type u_5} [inst : PartialOrder Γ] [inst_1 : SMul R V] [inst_2 : Zero V],
  (HahnModule.of R).symm 0 = 0
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
/-- Alternative formulation of `covariant_sequence_exact₁`  -/
CategoryTheory.Abelian.Ext.covariant_sequence_exact₁' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] (X : C) {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (n₀ n₁ : ℕ)
  (h : n₀ + 1 = n₁),
  { X₁ := AddCommGrpCat.of (CategoryTheory.Abelian.Ext X S.X₃ n₀),
      X₂ := AddCommGrpCat.of (CategoryTheory.Abelian.Ext X S.X₁ n₁),
      X₃ := AddCommGrpCat.of (CategoryTheory.Abelian.Ext X S.X₂ n₁),
      f := AddCommGrpCat.ofHom (hS.extClass.postcomp X h),
      g := AddCommGrpCat.ofHom ((CategoryTheory.Abelian.Ext.mk₀ S.f).postcomp X ⋯), zero := ⋯ }.Exact
-- Init.Data.UInt.Lemmas
UInt32.ofBitVec_pow : ∀ (a : BitVec 32) (n : ℕ), { toBitVec := a ^ n } = { toBitVec := a } ^ n
-- Init.Data.Int.DivMod.Lemmas
Int.add_neg_mul_bmod_self_left : ∀ (a : ℤ) (b : ℕ) (c : ℤ), (a + -(↑b * c)).bmod b = a.bmod b
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.single_P : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}} [inst_1 : Fact κ.IsRegular] (j a : J),
  (CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.single j).P a =
    CategoryTheory.ObjectProperty.ofObj (fun x => j) a
-- Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
sSup_one : ∀ {M : Type u_1} [inst : CompleteLattice M] [inst_1 : One M], sSup 1 = 1
-- Init.Data.Range.Polymorphic.Char
Char.instLawfulHasSize_2 : Std.Rxi.LawfulHasSize Char
-- Aesop.Script.SpecificTactics
_private.Aesop.Script.SpecificTactics.0.Aesop.splitTargetS?.tacticBuilder : Array Lean.MVarId → Aesop.Script.TacticBuilder
-- Mathlib.Algebra.Order.Monoid.Defs
IsOrderedAddMonoid.toAddRightMono : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : Preorder α] [IsOrderedAddMonoid α], AddRightMono α
-- Mathlib.Topology.PartialHomeomorph.Basic
PartialHomeomorph.source_inter_preimage_target_inter : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialHomeomorph X Y)
  (s : Set Y), e.source ∩ ↑e ⁻¹' (e.target ∩ s) = e.source ∩ ↑e ⁻¹' s
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.unflip_flip : ∀ {X : Type u_5} {α : Type u_6} {β : Type u_7} [inst : Finite α] [inst_1 : TopologicalSpace X]
  (f : LocallyConstant X (α → β)), LocallyConstant.unflip f.flip = f
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.iteratedSliceForwardNaturalityIso_inv_app : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Over X} (p : f ⟶ g)
  (X_1 : CategoryTheory.Over f),
  (CategoryTheory.Over.iteratedSliceForwardNaturalityIso p).inv.app X_1 =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.Over.map (CategoryTheory.Over.Hom.left p)).obj
        (CategoryTheory.Over.mk (CategoryTheory.Over.Hom.left X_1.hom)))
-- Mathlib.Algebra.Star.StarProjection
/-- A star projection is a self-adjoint idempotent.  -/
IsStarProjection : {R : Type u_1} → [Mul R] → [Star R] → R → Prop
-- Mathlib.GroupTheory.GroupAction.Basic
/-- The isomorphism between the stabilizers of two elements in the same orbit.  -/
AddAction.stabilizerEquivStabilizer : {G : Type u_1} →
  {α : Type u_2} →
    [inst : AddGroup G] →
      [inst_1 : AddAction G α] →
        {g : G} → {a b : α} → b = g +ᵥ a → ↥(AddAction.stabilizer G a) ≃+ ↥(AddAction.stabilizer G b)
-- Mathlib.RingTheory.WittVector.Defs
WittVector.mk' : {p : ℕ} → {R : Type u_1} → (ℕ → R) → WittVector p R
-- Init.Data.UInt.Lemmas
UInt8.ofNat_mod : ∀ {a b : ℕ}, a < 2 ^ 8 → b < 2 ^ 8 → UInt8.ofNat (a % b) = UInt8.ofNat a % UInt8.ofNat b
-- Std.Time.DateTime
/-- Determines the era of the given `DateTime` based on its year.
 -/
Std.Time.DateTime.era : Std.Time.DateTime → Std.Time.Year.Era
-- Mathlib.Tactic.GRewrite.Core
/-- The proof of the implication. The direction depends on the argument `forwardImp`.  -/
Mathlib.Tactic.GRewrite.GRewriteResult.impProof : Mathlib.Tactic.GRewrite.GRewriteResult → Lean.Expr
-- Init.Data.UInt.Lemmas
UInt32.ofBitVec_neg : ∀ (b : BitVec 32), { toBitVec := -b } = -{ toBitVec := b }
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whiskerRight_id_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  (f : X ⟶ Y) {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Y (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight f (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom
      (CategoryTheory.CategoryStruct.comp f
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).inv h))
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.comap_map_mk' : ∀ {G : Type u} [inst : Group G] (N H : Subgroup G) [inst_1 : N.Normal],
  Subgroup.comap (QuotientGroup.mk' N) (Subgroup.map (QuotientGroup.mk' N) H) = N ⊔ H
-- Init.System.IO
/-- Reads text up to and including the next newline from the stream.

If the returned string is empty, an end-of-file marker (EOF) has been reached.
An EOF does not actually close a stream, so further reads may block and return more data.
 -/
IO.FS.Stream.getLine : IO.FS.Stream → IO String
-- Mathlib.Data.Bundle
Bundle.TotalSpace.mk_cast : ∀ {B : Type u_1} {F : Type u_2} {E : B → Type u_3} {x x' : B} (h : x = x') (b : E x), ⟨x', cast ⋯ b⟩ = ⟨x, b⟩
-- Mathlib.Combinatorics.Quiver.Covering
Prefunctor.isCovering_of_bijective_star : ∀ {U : Type u_1} [inst : Quiver U] {V : Type u_2} [inst_1 : Quiver V] (φ : U ⥤q V)
  [inst_2 : Quiver.HasInvolutiveReverse U] [inst_3 : Quiver.HasInvolutiveReverse V] [φ.MapReverse],
  (∀ (u : U), Function.Bijective (φ.star u)) → φ.IsCovering
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
DiscreteConvolution.mulFiber_one_mem : ∀ {M : Type u_1} [inst : Monoid M], (1, 1) ∈ DiscreteConvolution.mulFiber 1
-- Mathlib.AlgebraicGeometry.FunctionField
AlgebraicGeometry.Scheme.algebraMap_germ_eq_germToFunctionField : ∀ (X : AlgebraicGeometry.Scheme) [inst : IrreducibleSpace ↥X] {U : X.Opens} [inst_1 : Nonempty ↥↑U] {x : ↥X}
  (hx : x ∈ U) (f : ↑(X.presheaf.obj (Opposite.op U))),
  (algebraMap ↑(X.presheaf.stalk x) ↑X.functionField)
      ((CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U x hx)) f) =
    (CategoryTheory.ConcreteCategory.hom (X.germToFunctionField U)) f
-- Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
CategoryTheory.SmallObject.SuccStruct.extendToSuccObjIso_hom_naturality_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {J : Type u} [inst_1 : LinearOrder J]
  [inst_2 : SuccOrder J] {j : J} (hj : ¬IsMax j) (F : CategoryTheory.Functor (↑(Set.Iic j)) C) {X : C}
  (τ : F.obj ⟨j, ⋯⟩ ⟶ X) (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ ≤ j) {Z : C} (h : F.obj ⟨i₂, hi₂⟩ ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.SmallObject.SuccStruct.extendToSucc hj F τ).map (CategoryTheory.homOfLE hi))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.SuccStruct.extendToSuccObjIso hj F τ i₂ hi₂).hom
        h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.SuccStruct.extendToSuccObjIso hj F τ i₁ ⋯).hom
      (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.homOfLE hi)) h)
-- Mathlib.Order.ConditionallyCompleteLattice.Finset
sSup_ne_top : ∀ {α : Type u_5} [inst : CompleteLinearOrder α] [Nontrivial α] {s : Set α}, s.Finite → ⊤ ∉ s → sSup s ≠ ⊤
-- Init.Data.Option.Basic
/-- Returns `true` on `none` and `false` on `some x`.

This function is more flexible than `(· == none)` because it does not require a `BEq α` instance.

Examples:
* `(none : Option Nat).isNone = true`
* `(some Nat.add).isNone = false`
 -/
Option.isNone : {α : Type u_1} → Option α → Bool
-- Mathlib.Algebra.Order.Ring.Ordering.Defs
RingPreordering.toSubsemiring : {R : Type u_1} → [inst : CommRing R] → RingPreordering R → Subsemiring R
-- Aesop.EMap
Aesop.EMap.mk.injEq : ∀ {α : Type u_1} (rep : Lean.PArray (Option (Lean.Expr × α))) (idx : Lean.Meta.DiscrTree ℕ)
  (rep_1 : Lean.PArray (Option (Lean.Expr × α))) (idx_1 : Lean.Meta.DiscrTree ℕ),
  ({ rep := rep, idx := idx } = { rep := rep_1, idx := idx_1 }) = (rep = rep_1 ∧ idx = idx_1)
-- Mathlib.Algebra.GroupWithZero.Action.Pi
Pi.smulWithZero : {I : Type u} →
  {f : I → Type v} →
    (α : Type u_1) →
      [inst : Zero α] →
        [inst_1 : (i : I) → Zero (f i)] → [(i : I) → SMulWithZero α (f i)] → SMulWithZero α ((i : I) → f i)
-- Mathlib.Geometry.Manifold.PartitionOfUnity
/-- A `BumpCovering` such that all functions in this covering are smooth generates a smooth
partition of unity.

In our formalization, not every `f : BumpCovering ι M s` with smooth functions `f i` is a
`SmoothBumpCovering`; instead, a `SmoothBumpCovering` is a covering by supports of
`SmoothBumpFunction`s. So, we define `BumpCovering.toSmoothPartitionOfUnity`, then reuse it
in `SmoothBumpCovering.toSmoothPartitionOfUnity`.  -/
BumpCovering.toSmoothPartitionOfUnity : {ι : Type uι} →
  {E : Type uE} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        {H : Type uH} →
          [inst_2 : TopologicalSpace H] →
            {I : ModelWithCorners ℝ E H} →
              {M : Type uM} →
                [inst_3 : TopologicalSpace M] →
                  [inst_4 : ChartedSpace H M] →
                    {s : Set M} →
                      (f : BumpCovering ι M s) →
                        (∀ (i : ι), ContMDiff I (modelWithCornersSelf ℝ ℝ) ↑⊤ ⇑(f i)) → SmoothPartitionOfUnity ι I M s
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
/-- The continuous linear map given by `(x, y) ↦ f₁ x + f₂ y`.  -/
ContinuousLinearMap.coprod : {R : Type u_1} →
  {M : Type u_3} →
    {M₁ : Type u_5} →
      {M₂ : Type u_6} →
        [inst : Semiring R] →
          [inst_1 : TopologicalSpace M] →
            [inst_2 : TopologicalSpace M₁] →
              [inst_3 : TopologicalSpace M₂] →
                [inst_4 : AddCommMonoid M] →
                  [inst_5 : Module R M] →
                    [ContinuousAdd M] →
                      [inst_7 : AddCommMonoid M₁] →
                        [inst_8 : Module R M₁] →
                          [inst_9 : AddCommMonoid M₂] →
                            [inst_10 : Module R M₂] → (M₁ →L[R] M) → (M₂ →L[R] M) → M₁ × M₂ →L[R] M
-- Mathlib.LinearAlgebra.Basis.Bilinear
/-- Write out `B x y` as a sum over `B (b i) (b j)` if `b` is a basis.

Version for semi-bilinear maps, see `sum_repr_mul_repr_mul` for the bilinear version.  -/
LinearMap.sum_repr_mul_repr_mulₛₗ : ∀ {ι₁ : Type u_1} {ι₂ : Type u_2} {R : Type u_3} {R₂ : Type u_4} {S : Type u_5} {S₂ : Type u_6} {M : Type u_7}
  {N : Type u_8} {P : Type u_9} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Semiring R₂] [inst_3 : Semiring S₂]
  [inst_4 : AddCommMonoid M] [inst_5 : AddCommMonoid N] [inst_6 : AddCommMonoid P] [inst_7 : Module R M]
  [inst_8 : Module S N] [inst_9 : Module R₂ P] [inst_10 : Module S₂ P] [inst_11 : SMulCommClass S₂ R₂ P]
  {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} (b₁ : Module.Basis ι₁ R M) (b₂ : Module.Basis ι₂ S N) {B : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P}
  (x : M) (y : N),
  ((b₁.repr x).sum fun i xi => (b₂.repr y).sum fun j yj => ρ₁₂ xi • σ₁₂ yj • (B (b₁ i)) (b₂ j)) = (B x) y