mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.RightUnitorBimod.hom_right_act_hom' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C] {R S : CategoryTheory.Mon C} (P : Bimod R S)
  [inst_3 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorLeft X)]
  [inst_4 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorRight X)],
  CategoryTheory.CategoryStruct.comp (P.tensorBimod (Bimod.regular S)).actRight (Bimod.RightUnitorBimod.hom P) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (Bimod.RightUnitorBimod.hom P) S.X) P.actRight
-- Mathlib.RingTheory.Congruence.Defs
RingCon.instAddZeroClassQuotient : {R : Type u_1} → [inst : AddZeroClass R] → [inst_1 : Mul R] → (c : RingCon R) → AddZeroClass c.Quotient
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.LaxBraidedFunctor.hom_ext_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.MonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  {F G : CategoryTheory.LaxBraidedFunctor C D} {α β : F ⟶ G}, α = β ↔ α.hom.hom = β.hom.hom
-- Std.Data.Internal.Cut
Std.Internal.IsStrictCut.toIsCut : ∀ {α : Type u} {cmp : α → α → Ordering} {cut : α → Ordering} [self : Std.Internal.IsStrictCut cmp cut],
  Std.Internal.IsCut cmp cut
-- Mathlib.Order.SuccPred.Archimedean
WellFoundedGT.toIsSuccArchimedean : ∀ {α : Type u_1} [inst : PartialOrder α] [h : WellFoundedGT α] [inst_1 : SuccOrder α], IsSuccArchimedean α
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.support_bot : ∀ {X : AlgebraicGeometry.Scheme}, ⊥.support = ⊤
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.intermediateFieldMap_apply_coe : ∀ {K : Type u_1} {L : Type u_2} {L' : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Field L']
  [inst_3 : Algebra K L] [inst_4 : Algebra K L'] (e : L ≃ₐ[K] L') (E : IntermediateField K L) (a : ↥E),
  ↑((IntermediateField.intermediateFieldMap e E) a) = e ↑a
-- Mathlib.Algebra.Homology.EulerCharacteristic
/-- If a graded object has finite rank support contained in a finite set,
the `finsum` Euler characteristic equals the finite sum over that set.  -/
GradedObject.eulerChar_eq_sum_finSet_of_finrankSupport_subset : ∀ {R : Type u_1} [inst : Ring R] {ι : Type u_2} (c : ComplexShape ι) [inst_1 : c.EulerCharSigns]
  (X : CategoryTheory.GradedObject ι (ModuleCat R)) (indices : Finset ι),
  GradedObject.finrankSupport X ⊆ ↑indices →
    GradedObject.eulerChar c X = ∑ i ∈ indices, ↑(c.χ i) * ↑(Module.finrank R ↑(X i))
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.powerlt_mono_left : ∀ (a : Cardinal.{u_1}), Monotone fun c => a ^< c
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem!_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} [inst_2 : Inhabited β], k ∉ m₁ → (m₁ ∪ m₂)[k]! = m₂[k]!
-- Lean.Util.FindExpr
/-- Do not search subterms  -/
Lean.Expr.FindStep.done : Lean.Expr.FindStep
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.iteratedFDerivLM_eq_of_scalars : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] {n k : ℕ∞} {K : TopologicalSpace.Compacts E} {i : ℕ} (𝕜' : Type u_5)
  [inst_7 : NontriviallyNormedField 𝕜'] [inst_8 : NormedSpace 𝕜' F] [inst_9 : SMulCommClass ℝ 𝕜' F],
  ⇑(ContDiffMapSupportedIn.iteratedFDerivLM 𝕜 n k i) = ⇑(ContDiffMapSupportedIn.iteratedFDerivLM 𝕜' n k i)
-- Mathlib.Algebra.Order.Sub.Unbundled.Hom
AddMonoidHom.le_map_tsub : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : AddCommMonoid α] [inst_2 : Sub α] [OrderedSub α]
  [inst_4 : Preorder β] [inst_5 : AddZeroClass β] [inst_6 : Sub β] [OrderedSub β] (f : α →+ β),
  Monotone ⇑f → ∀ (a b : α), f a - f b ≤ f (a - b)
-- Mathlib.GroupTheory.Index
AddSubgroup.finiteIndex_iInf' : ∀ {G : Type u_1} [inst : AddGroup G] {ι : Type u_3} {s : Finset ι} (f : ι → AddSubgroup G),
  (∀ i ∈ s, (f i).FiniteIndex) → (⨅ i ∈ s, f i).FiniteIndex
-- Mathlib.LinearAlgebra.AffineSpace.Midpoint
midpoint_eq_midpoint_iff_vsub_eq_vsub : ∀ (R : Type u_1) {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] {x x' y y' : P}, midpoint R x y = midpoint R x' y' ↔ x -ᵥ x' = y' -ᵥ y
-- Mathlib.Algebra.Order.UpperLower
IsLowerSet.vadd : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Preorder α] [IsOrderedAddMonoid α] {s : Set α} {a : α},
  IsLowerSet s → IsLowerSet (a +ᵥ s)
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_orElse_Option_apply_eq : ∀ {α : Type u_1} (x : Option α) (h : Unit → Option α) (post : α → Prop) (epost : Prop),
  Std.Internal.Do.wp (OrElse.orElse x h) post epost = Std.Internal.Do.wp x post (Std.Internal.Do.wp (h ()) post epost)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.card_mul_singleton : ∀ {α : Type u_2} [inst : Mul α] [IsRightCancelMul α] [inst_2 : DecidableEq α] (s : Finset α) (a : α),
  (s * {a}).card = s.card
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Triangle.sbtw_touchpoint_empty : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (t : Affine.Triangle ℝ P) {i₁ i₂ i₃ : Fin 3},
  i₁ ≠ i₂ → i₁ ≠ i₃ → i₂ ≠ i₃ → Sbtw ℝ (t.points i₁) (Affine.Simplex.touchpoint t ∅ i₂) (t.points i₃)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Reify
_private.Lean.Meta.Tactic.Grind.Arith.Linear.Reify.0.Lean.Meta.Grind.Arith.Linear.assertNatCastNonneg : Lean.Expr → Lean.Meta.Grind.Arith.Linear.LinearM Unit
-- Mathlib.CategoryTheory.ObjectProperty.Shift
CategoryTheory.ObjectProperty.shiftClosure_le_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P Q : CategoryTheory.ObjectProperty C) {A : Type u_2}
  [inst_1 : AddMonoid A] [inst_2 : CategoryTheory.HasShift C A] [Q.IsClosedUnderIsomorphisms] [Q.IsStableUnderShift A],
  P.shiftClosure A ≤ Q ↔ P ≤ Q
-- Mathlib.Algebra.Category.CommHopfAlgCat
CommHopfAlgCat.instCategory : {R : Type u} → [inst : CommRing R] → CategoryTheory.Category.{v, max (v + 1) u} (CommHopfAlgCat R)
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
TendstoUniformlyOn.div : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Type u_3}
  {l : Filter ι} {f f' : ι → β → α} {g g' : β → α} {s : Set β},
  TendstoUniformlyOn f g l s → TendstoUniformlyOn f' g' l s → TendstoUniformlyOn (f / f') (g / g') l s
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.smul_sup : ∀ {R : Type u_1} {E : Type u_3} [inst : AddGroup E] [inst_1 : SMul R ℝ] [inst_2 : SMul R NNReal]
  [inst_3 : IsScalarTower R NNReal ℝ] (r : R) (p q : AddGroupSeminorm E), r • (p ⊔ q) = r • p ⊔ r • q
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.coe_rescaleAlgHom : ∀ {R : Type u_2} [inst : CommRing R] (r : R), ↑(PowerSeries.rescaleAlgHom r) = PowerSeries.rescale r
-- Init.Data.Int.Gcd
Int.lcm_mul_right_right : ∀ (a b : ℤ), a.lcm (a * b) = a.natAbs * b.natAbs
-- Init.Data.UInt.Lemmas
UInt32.lt_add_one : ∀ {c : UInt32}, c ≠ -1 → c < c + 1
-- Mathlib.Data.PNat.Factors
/-- The product of a `PrimeMultiset`, as a `ℕ+`.  -/
PrimeMultiset.prod : PrimeMultiset → ℕ+
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.ToForwardSearcher.mk : {ρ : Type} →
  {pat : ρ} →
    {σ : outParam (String.Slice → Type)} →
      ((s : String.Slice) → Std.Iter (String.Slice.Pattern.SearchStep s)) → String.Slice.Pattern.ToForwardSearcher pat σ
-- Mathlib.Algebra.Group.Units.Defs
Units.inv_eq_val_inv : ∀ {α : Type u} [inst : Monoid α] (a : αˣ), a.inv = ↑a⁻¹
-- Mathlib.MeasureTheory.Function.L2Space
MeasureTheory.L2.instInnerSubtypeAEEqFunMemAddSubgroupLpOfNatENNReal : {α : Type u_1} →
  {E : Type u_2} →
    {𝕜 : Type u_4} →
      [inst : RCLike 𝕜] →
        {m : MeasurableSpace α} →
          {μ : MeasureTheory.Measure α} →
            [inst_1 : NormedAddCommGroup E] → [InnerProductSpace 𝕜 E] → Inner 𝕜 ↥(MeasureTheory.Lp E 2 μ)
-- Mathlib.Data.Nat.Factors
Nat.eq_two_pow_or_exists_odd_prime_and_dvd : ∀ (n : ℕ), (∃ k, n = 2 ^ k) ∨ ∃ p, Nat.Prime p ∧ p ∣ n ∧ Odd p
-- Mathlib.FieldTheory.SeparableDegree
IntermediateField.isSeparable_of_mem_isSeparable : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {L : IntermediateField F E}
  [Algebra.IsSeparable F ↥L] {x : E}, x ∈ L → IsSeparable F x
-- Mathlib.LinearAlgebra.RootSystem.Reduced
RootPairing.nsmul_notMem_range_root : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) [CharZero R]
  [IsAddTorsionFree M] [P.IsReduced] {n : ℕ} [n.AtLeastTwo] {i : ι}, n • P.root i ∉ Set.range ⇑P.root
-- Mathlib.Analysis.Normed.Group.Continuity
Continuous.enorm : ∀ {E : Type u_7} [inst : TopologicalSpace E] [inst_1 : ContinuousENorm E] {X : Type u_8} [inst_2 : TopologicalSpace X]
  {f : X → E}, Continuous f → Continuous fun x => ‖f x‖ₑ
-- Mathlib.Order.Category.CompleteLat
/-- Constructs an isomorphism of complete lattices from an order isomorphism between them.  -/
CompleteLat.Iso.mk : {α β : CompleteLat} → ↑α ≃o ↑β → (α ≅ β)
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.EnrichedFunctor.comp_map : ∀ (V : Type v) [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₁}
  {D : Type u₂} {E : Type u₃} [inst_2 : CategoryTheory.EnrichedCategory V C]
  [inst_3 : CategoryTheory.EnrichedCategory V D] [inst_4 : CategoryTheory.EnrichedCategory V E]
  (F : CategoryTheory.EnrichedFunctor V C D) (G : CategoryTheory.EnrichedFunctor V D E) (x x_1 : C),
  (CategoryTheory.EnrichedFunctor.comp V F G).map x x_1 =
    CategoryTheory.CategoryStruct.comp (F.map x x_1) (G.map (F.obj x) (F.obj x_1))
-- Mathlib.CategoryTheory.Bicategory.Monad.Basic
/-- The oplax functor from the trivial bicategory to `B` associated with the comonad.  -/
CategoryTheory.Bicategory.OplaxTrans.ComonadBicat.toOplax : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    CategoryTheory.Bicategory.OplaxTrans.ComonadBicat B →
      CategoryTheory.OplaxFunctor (CategoryTheory.LocallyDiscrete (CategoryTheory.Discrete PUnit.{1})) B
-- Mathlib.Topology.Order.MonotoneConvergence
tendsto_atTop_iSup : ∀ {α : Type u_1} {ι : Type u_3} [inst : Preorder ι] [inst_1 : TopologicalSpace α] [inst_2 : CompleteLattice α]
  [SupConvergenceClass α] {f : ι → α}, Monotone f → Filter.Tendsto f Filter.atTop (nhds (⨆ i, f i))
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.isCongruent.goEq : Lean.Meta.Grind.ENodeMap → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Bool
-- Mathlib.Order.Nucleus
Nucleus.coe_toInfHom : ∀ {X : Type u_1} [inst : SemilatticeInf X] (n : Nucleus X), ⇑n.toInfHom = ⇑n
-- Mathlib.Analysis.Calculus.Implicit
ImplicitFunctionData.hasStrictFDerivAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {G : Type u_4} [inst_7 : NormedAddCommGroup G]
  [inst_8 : NormedSpace 𝕜 G] [inst_9 : CompleteSpace G] (φ : ImplicitFunctionData 𝕜 E F G),
  HasStrictFDerivAt φ.prodFun (↑(φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv ⋯ ⋯ ⋯)) φ.pt
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.toLp.eq_1 : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] [inst_4 : MeasurableSpace E] [inst_5 : OpensMeasurableSpace E]
  [inst_6 : SecondCountableTopologyEither E F] (f : SchwartzMap E F) (p : ENNReal) (μ : MeasureTheory.Measure E)
  [hμ : μ.HasTemperateGrowth], f.toLp p μ = MeasureTheory.MemLp.toLp ⇑f ⋯
-- Mathlib.Data.List.Chain
/-- Given a chain `l`, such that a predicate `p` holds for its head if it is nonempty,
and if `r x y → p x → p y`, then the predicate is true everywhere in the chain.
That is, we can propagate the predicate down the chain.
 -/
List.IsChain.induction : ∀ {α : Type u_1} {r : α → α → Prop} (p : α → Prop) (l : List α),
  List.IsChain r l → (∀ ⦃x y : α⦄, r x y → p x → p y) → (∀ (lne : l ≠ []), p (l.head lne)) → ∀ i ∈ l, p i
-- Mathlib.RingTheory.RamificationInertia.Inertia
Ideal.inertiaDeg_tower : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T] (q : Ideal S) (r : Ideal T)
  [r.LiesOver q], r.inertiaDeg R = q.inertiaDeg R * r.inertiaDeg S
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- The underlying object of an object in `Over X`.  -/
CategoryTheory.Over.left : {T : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} T] → {X : T} → CategoryTheory.Over X → T
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.insertMany_nil : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β),
  ↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m []) = m
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.symmetryIso_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {Y : D} {b : C} {f' : F.obj b ⟶ Y} (hf' : F.relativelyRepresentable f') {a : C}
  {g : F.obj a ⟶ Y} (hg : F.relativelyRepresentable g) [inst_2 : F.Full] [inst_3 : F.Faithful],
  (hf'.symmetryIso hg).inv = hg.symmetry hf'
-- Init.Data.List.Lemmas
List.dropLast_append_cons : ∀ {α : Type u_1} {l₁ : List α} {b : α} {l₂ : List α}, (l₁ ++ b :: l₂).dropLast = l₁ ++ (b :: l₂).dropLast
-- Batteries.Data.Array.Scan
Subarray.scanlM.eq_1 : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [inst : Monad m] (f : β → α → m β) (init : β)
  (as : Subarray α), Subarray.scanlM f init as = Array.scanlM f init as.array as.start as.stop
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.sum_fintype : ∀ {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} [inst : Fintype ι] (μ : ι → MeasureTheory.Measure α),
  MeasureTheory.Measure.sum μ = ∑ i, μ i
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.preimage_add_right_zero' : ∀ {α : Type u_2} [inst : AddGroup α] {b : α}, Finset.preimage 0 (fun x => x + -b) ⋯ = {b}
-- Mathlib.LinearAlgebra.Isomorphisms
LinearMap.quotKerEquivOfSurjective_symm_apply : ∀ {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] (f : M →ₗ[R] M₂) (hf : Function.Surjective ⇑f) (x : M),
  (f.quotKerEquivOfSurjective hf).symm (f x) = Submodule.Quotient.mk x
-- Mathlib.Algebra.Free
FreeAddMagma.add : {α : Type u} → FreeAddMagma α → FreeAddMagma α → FreeAddMagma α
-- Mathlib.Combinatorics.Quiver.ConnectedComponent
/-- Positive strong connectivity: every ordered pair of vertices is joined by a directed path
of positive length.  -/
Quiver.IsSStronglyConnected : (V : Type u_2) → [Quiver V] → Prop
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.zero_apply : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (x : R), ↑0 x = 0
-- Mathlib.Algebra.Group.End
MulAut.instInhabited.eq_1 : ∀ (M : Type u_2) [inst : Mul M], MulAut.instInhabited M = { default := 1 }
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.comp.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  {X Y Z : CategoryTheory.Grothendieck F} (f : X.Hom Y) (g : Y.Hom Z),
  CategoryTheory.Grothendieck.comp f g =
    { base := CategoryTheory.CategoryStruct.comp f.base g.base,
      fiber :=
        CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
          (CategoryTheory.CategoryStruct.comp ((F.map g.base).toFunctor.map f.fiber) g.fiber) }
-- Init.Data.List.Erase
_private.Init.Data.List.Erase.0.List.eraseP_filterMap.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : (y : β) → motive (some y)) (h_2 : Unit → motive none),
  (match none with
    | some y => h_1 y
    | none => h_2 ()) =
    h_2 ()
-- Lean.Meta.Tactic.Grind.Arith.Linear.LinearM
Lean.Meta.Grind.Arith.Linear.instMonadGetStructLinearM : Lean.Meta.Grind.Arith.Linear.MonadGetStruct Lean.Meta.Grind.Arith.Linear.LinearM
-- Mathlib.Algebra.Opposites
MulOpposite.instAdd : {α : Type u_1} → [Add α] → Add αᵐᵒᵖ
-- Mathlib.Topology.ContinuousOn
ContinuousOn.prodMk : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] {f : α → β} {g : α → γ} {s : Set α},
  ContinuousOn f s → ContinuousOn g s → ContinuousOn (fun x => (f x, g x)) s
-- Mathlib.Data.Set.Opposite
/-- The members of the opposite of a set are in bijection with the members of the set itself.  -/
Set.opEquiv_self : {α : Type u_1} → (s : Set α) → ↑s.op ≃ ↑s
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Complex.sin_surjective : Function.Surjective Complex.sin
-- Mathlib.Order.InitialSeg
/-- Any element of a well order yields a principal segment.  -/
PrincipalSeg.ofElement : {α : Type u_4} → (r : α → α → Prop) → (a : α) → PrincipalSeg (Subrel r fun x => r x a) r
-- Mathlib.Algebra.Colimit.Module
AddCon.ker.congr_simp : ∀ {M : Type u_1} {N : Type u_2} {F : Type u_4} [inst : Add M] [inst_1 : Add N] [inst_2 : FunLike F M N]
  [inst_3 : AddHomClass F M N] (f f_1 : F), f = f_1 → AddCon.ker f = AddCon.ker f_1
-- Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
/-- **Alias** of `CategoryTheory.SemiCartesianMonoidalCategory.fst`. -/
CategoryTheory.Functor.chosenProd.fst : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    [self : CategoryTheory.SemiCartesianMonoidalCategory C] →
      (X Y : C) → CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ X
-- Mathlib.GroupTheory.IndexNSmul
/-- On an additive group that is torsion-free as a `ℤ`-module, the linear map given by
multiplication by `n : ℕ` is injective (when `n ≠ 0`).  -/
AddSubgroup.distribSMulToLinearMap_injective_of_isTorsionFree : ∀ {M : Type u_1} [inst : AddCommGroup M] [Module.IsTorsionFree ℤ M] {n : ℕ},
  n ≠ 0 → Function.Injective ⇑(DistribSMul.toLinearMap ℤ M n)
-- Mathlib.CategoryTheory.Sites.SheafOfTypes
/-- Construct a family of elements from a cocone.  -/
CategoryTheory.Presieve.yonedaFamilyOfElements_fromCocone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} →
      (R : CategoryTheory.Presieve X) →
        (s : CategoryTheory.Limits.Cocone R.diagram) →
          CategoryTheory.Presieve.FamilyOfElements (CategoryTheory.yoneda.obj s.pt) R
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
AffineSubspace.smul_vsub_vadd_mem : ∀ {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) (c : k) {p₁ p₂ p₃ : P},
  p₁ ∈ s → p₂ ∈ s → p₃ ∈ s → c • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ s
-- Init.Data.Iterators.Combinators.Monadic.FlatMap
Std.Iterators.Types.Flatten.IsPlausibleStep.outerYield : ∀ {α α₂ β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m (Std.IterM m β)] [inst_1 : Std.Iterator α₂ m β]
  {it₁ it₁' : Std.IterM m (Std.IterM m β)} {it₂' : Std.IterM m β},
  it₁.IsPlausibleStep (Std.IterStep.yield it₁' it₂') →
    Std.Iterators.Types.Flatten.IsPlausibleStep { internalState := { it₁ := it₁, it₂ := none } }
      (Std.IterStep.skip { internalState := { it₁ := it₁', it₂ := some it₂' } })
-- Mathlib.Data.ENNReal.Inv
ENNReal.add_halves : ∀ (a : ENNReal), a / 2 + a / 2 = a
-- Mathlib.Data.Finset.Image
Finset.map_insert : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst_1 : DecidableEq β] (f : α ↪ β) (a : α) (s : Finset α),
  Finset.map f (insert a s) = insert (f a) (Finset.map f s)
-- Mathlib.RingTheory.Congruence.BigOperators
RingCon.finsuppProd : ∀ {ι : Type u_1} {β : Type u_2} {M : Type u_3} [inst : Add M] [inst_1 : CommMonoid M] [inst_2 : Zero β] (c : RingCon M)
  (h h' : ι → β → M) {f g : ι →₀ β},
  (∀ (i : ι), c (h i 0) 1) →
    (∀ (i : ι), c (h' i 0) 1) → (∀ (i : ι), c (h i (f i)) (h' i (g i))) → c (f.prod h) (g.prod h')
-- Mathlib.Combinatorics.SimpleGraph.Basic
/-- The supremum of two graphs `x ⊔ y` has edges where either `x` or `y` have edges.  -/
SimpleGraph.instMax : {V : Type u} → Max (SimpleGraph V)
-- Mathlib.Algebra.Ring.CompTypeclasses
RingHomId.eq_id : ∀ {R : Type u_4} {inst : Semiring R} {σ : R →+* R} [self : RingHomId σ], σ = RingHom.id R
-- Mathlib.Topology.Bases
TopologicalSpace.IsTopologicalBasis.of_isOpen_of_subset : ∀ {α : Type u} [t : TopologicalSpace α] {s s' : Set (Set α)},
  (∀ u ∈ s', IsOpen u) → TopologicalSpace.IsTopologicalBasis s → s ⊆ s' → TopologicalSpace.IsTopologicalBasis s'
-- Mathlib.LinearAlgebra.Pi
/-- Linear equivalence between linear functions `Rⁿ → M` and `Mⁿ`. The spaces `Rⁿ` and `Mⁿ`
are represented as `ι → R` and `ι → M`, respectively, where `ι` is a finite type.

This as an `S`-linear equivalence, under the assumption that `S` acts on `M` commuting with `R`.
When `R` is commutative, we can take this to be the usual action with `S = R`.
Otherwise, `S = ℕ` shows that the equivalence is additive.
See note [bundled maps over different rings].  -/
LinearEquiv.piRing : (R : Type u) →
  (M : Type v) →
    (ι : Type x) →
      [inst : Semiring R] →
        (S : Type u_4) →
          [Fintype ι] →
            [DecidableEq ι] →
              [inst_3 : Semiring S] →
                [inst_4 : AddCommMonoid M] →
                  [inst_5 : Module R M] →
                    [inst_6 : Module S M] → [inst_7 : SMulCommClass R S M] → ((ι → R) →ₗ[R] M) ≃ₗ[S] ι → M
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKeyD_le_maxKeyD_insertEntry : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    l.isEmpty = false →
      ∀ {k : α} {v : β k} {fallback : α},
        (compare (Std.Internal.List.maxKeyD l fallback)
              (Std.Internal.List.maxKeyD (Std.Internal.List.insertEntry k v l) fallback)).isLE =
          true
-- Init.Grind.Interactive
/-- `admit` is a synonym for `sorry`.  -/
Lean.Parser.Tactic.Grind.grindAdmit : Lean.ParserDescr
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.prod_ite_of_false : ∀ {ι : Type u_1} {M : Type u_3} {s : Finset ι} [inst : CommMonoid M] {p : ι → Prop} [inst_1 : DecidablePred p],
  (∀ x ∈ s, ¬p x) → ∀ (f g : ι → M), (∏ x ∈ s, if p x then f x else g x) = ∏ x ∈ s, g x
-- Mathlib.Topology.Algebra.Group.Basic
topologicalAddGroup_inf : ∀ {G : Type w} [inst : AddGroup G] {t₁ t₂ : TopologicalSpace G},
  IsTopologicalAddGroup G → IsTopologicalAddGroup G → IsTopologicalAddGroup G
-- Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology
/-- **Alias** of the forward direction of `ContinuousLinearMapWOT.continuous_iff`. -/
ContinuousLinearMapWOT.continuous_inner_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E]
  [inst_3 : Module 𝕜 E] [inst_4 : NormedAddCommGroup F] [inst_5 : InnerProductSpace 𝕜 F] [CompleteSpace F]
  {α : Type u_4} [inst_7 : TopologicalSpace α] {f : α → E →WOT[𝕜] F},
  Continuous f → ∀ (x : E) (y : F), Continuous fun x_1 => inner 𝕜 y ((f x_1) x)