mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.mem_comap : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {S : Subsemigroup N} {f : M →ₙ* N} {x : M},
  x ∈ Subsemigroup.comap f S ↔ f x ∈ S
-- Init.Data.Array.Attach
Array.countP_attach : ∀ {α : Type u_1} {xs : Array α} {p : α → Bool}, Array.countP (fun a => p ↑a) xs.attach = Array.countP p xs
-- Init.Data.Vector.Lemmas
Vector.sum_eq_foldr : ∀ {α : Type u_1} {n : ℕ} [inst : Add α] [inst_1 : Zero α] {xs : Vector α n},
  xs.sum = Vector.foldr (fun x1 x2 => x1 + x2) 0 xs
-- Mathlib.Algebra.MvPolynomial.PDeriv
/-- **Alias** of `MvPolynomial.pderiv_sumRingEquiv`. -/
MvPolynomial.pderiv_sumToIter : ∀ {R : Type u} [inst : CommSemiring R] {σ : Type u_1} {ι : Type u_2} (p : MvPolynomial (σ ⊕ ι) R) (i : σ),
  (MvPolynomial.pderiv i) ((MvPolynomial.sumRingEquiv R σ ι) p) =
    (MvPolynomial.sumRingEquiv R σ ι) ((MvPolynomial.pderiv (Sum.inl i)) p)
-- Mathlib.CategoryTheory.SingleObj
CategoryTheory.SingleObj.mapHom_comp : ∀ {M : Type u} [inst : Monoid M] {N : Type v} [inst_1 : Monoid N] (f : M →* N) {P : Type w} [inst_2 : Monoid P]
  (g : N →* P),
  (CategoryTheory.SingleObj.mapHom M P) (g.comp f) =
    ((CategoryTheory.SingleObj.mapHom M N) f).comp ((CategoryTheory.SingleObj.mapHom N P) g)
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.IsNormal.bsup : ∀ {f : Ordinal.{max u_3 u_4} → Ordinal.{max u_4 u_5}},
  Order.IsNormal f →
    ∀ {o : Ordinal.{u_4}} (g : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_4 u_3}),
      o ≠ 0 → f (o.bsup g) = o.bsup fun a h => f (g a h)
-- Mathlib.CategoryTheory.Monoidal.Hopf_
CategoryTheory.HopfObj.one_antipode_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : C) [inst_3 : CategoryTheory.HopfObj A] {Z : C} (h : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one
      (CategoryTheory.CategoryStruct.comp CategoryTheory.HopfObj.antipode h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one h
-- Std.Http.Data.Request
Std.Http.Request.Head.mk.inj : ∀ {method : Std.Http.Method} {version : Std.Http.Version} {uri : Std.Http.RequestTarget} {headers : Std.Http.Headers}
  {method_1 : Std.Http.Method} {version_1 : Std.Http.Version} {uri_1 : Std.Http.RequestTarget}
  {headers_1 : Std.Http.Headers},
  { method := method, version := version, uri := uri, headers := headers } =
      { method := method_1, version := version_1, uri := uri_1, headers := headers_1 } →
    method = method_1 ∧ version = version_1 ∧ uri = uri_1 ∧ headers = headers_1
-- Init.Data.Iterators.Lemmas.Combinators.ULift
_private.Init.Data.Iterators.Lemmas.Combinators.ULift.0.Std.IterM.step_uLift.match_1.eq_3 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (h : it.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.done, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_3 h
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.isEmpty_inter_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.isEmpty = true → (t₁ ∩ t₂).isEmpty = true
-- Lean.Elab.Tactic.Omega.Core
/-- Constructs a proof that `s.sat' c v = true`  -/
Lean.Elab.Tactic.Omega.Justification.proof : {s : Lean.Omega.Constraint} →
  {c : Lean.Omega.Coeffs} →
    Lean.Expr →
      Array Lean.Elab.Tactic.Omega.Proof → Lean.Elab.Tactic.Omega.Justification s c → Lean.Elab.Tactic.Omega.Proof
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
RootPairing.rootForm_nondegenerate : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : CommRing R] [IsDomain R] [inst_5 : Module R M] [inst_6 : Module R N]
  (P : RootPairing ι R M N) [P.IsAnisotropic] [P.IsRootSystem], P.RootForm.Nondegenerate
-- Mathlib.RingTheory.Valuation.Extension
_private.Mathlib.RingTheory.Valuation.Extension.0.Valuation.HasExtension.termK₀ : Lean.ParserDescr
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_insertMany!_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] [inst : BEq α]
  [Std.LawfulBEqOrd α] [inst_2 : Std.LawfulEqOrd α],
  t.WF →
    ∀ {l : List ((a : α) × β a)} {k : α} {fallback : β k},
      (List.map Sigma.fst l).contains k = false → (↑(t.insertMany! l)).getD k fallback = t.getD k fallback
-- Mathlib.Algebra.Group.Int.Units
Int.eq_one_or_neg_one_of_mul_eq_one' : ∀ {u v : ℤ}, u * v = 1 → u = 1 ∧ v = 1 ∨ u = -1 ∧ v = -1
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
/-- A rational map from `X` to `Y` (`X ⤏ Y`) is an equivalence class of partial maps,
where two partial maps are equivalent if they are equal on a dense open subscheme.  -/
AlgebraicGeometry.Scheme.RationalMap : AlgebraicGeometry.Scheme → AlgebraicGeometry.Scheme → Type u
-- Mathlib.Topology.MetricSpace.Polish
TopologicalSpace.Opens.CompleteCopy.instCompleteSpace : ∀ {α : Type u_1} [inst : MetricSpace α] {s : TopologicalSpace.Opens α} [CompleteSpace α], CompleteSpace s.CompleteCopy
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Univ
Matrix.charpoly.univ_coeff_card : ∀ (R : Type u_1) (n : Type u_3) [inst : CommRing R] [inst_1 : Fintype n] [inst_2 : DecidableEq n],
  (Matrix.charpoly.univ R n).coeff (Fintype.card n) = 1
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.skeletonLT_I`. -/
Topology.CWComplex.skeletonLT_I : ∀ {X : Type u_1} [t : TopologicalSpace X] [inst : T2Space X] (C : Set X) {D : Set X}
  [inst_1 : Topology.RelCWComplex C D] (n : ℕ∞) (l : ℕ), (Topology.RelCWComplex.skeletonLT C n).I l = {x | ↑l < n}
-- Mathlib.Algebra.Group.Equiv.Opposite
MonoidHom.fromOpposite.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : MulOneClass M] [inst_1 : MulOneClass N] (f : M →* N)
  (hf : ∀ (x y : M), Commute (f x) (f y)),
  f.fromOpposite hf = { toFun := ⇑f ∘ MulOpposite.unop, map_one' := ⋯, map_mul' := ⋯ }
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey_minKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {hc : t.minKey! ∈ t}, t.getKey t.minKey! hc = t.minKey!
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedSubmonoid.instPartialOrder : {M : Type u_1} → [inst : MulOneClass M] → PartialOrder (SaturatedSubmonoid M)
-- Aesop.Rule.Forward
Aesop.instBEqForwardRulePriority.beq : Aesop.ForwardRulePriority → Aesop.ForwardRulePriority → Bool
-- Mathlib.Tactic.Linarith.Frontend
/-- Split conjunctions in hypotheses.  -/
Mathlib.Tactic.Linarith.LinarithConfig.splitHypotheses : Mathlib.Tactic.Linarith.LinarithConfig → Bool
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_inter_add_sdiff₀ : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasureTheory.NullMeasurableSet t μ →
    autoParam (μ s ≠ ⊤) MeasureTheory.measureReal_inter_add_sdiff₀._auto_1 → μ.real (s ∩ t) + μ.real (s \ t) = μ.real s
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.empty_div : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Div α] (s : Finset α), ∅ / s = ∅
-- Mathlib.Data.FunLike.Group
/-- A `FunLike` type is a commutative group if `β` is a commutative group.  -/
FunLike.commGroup : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : Mul F] →
          [inst_2 : One F] →
            [inst_3 : Pow F ℕ] →
              [inst_4 : Inv F] →
                [inst_5 : Div F] →
                  [inst_6 : Pow F ℤ] →
                    [inst_7 : CommGroup β] →
                      [IsOneApply F α β] →
                        [IsMulApply F α β] →
                          [IsInvApply F α β] →
                            [IsDivApply F α β] → [IsPowApply ℕ F α β] → [IsPowApply ℤ F α β] → CommGroup F
-- Init.Data.Range.Polymorphic.Char
_private.Init.Data.Range.Polymorphic.Char.0.Char.map : Std.PRange.UpwardEnumerable.Map Char (Fin Char.numCodePoints)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.coe_zpow : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : DivInvMonoid β] (f : MeasureTheory.SimpleFunc α β)
  (z : ℤ), ⇑(f ^ z) = ⇑f ^ z
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
/-- If `φ : K ⟶ L` is a morphism of cochain complexes in `C` and `G : C ⥤ D` is an
additive functor, then the image by `G` of the triangle `triangle φ` identifies to
the triangle associated to the image of `φ` by `G`.  -/
CochainComplex.mappingCone.mapTriangleIso : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [inst_2 : CategoryTheory.Preadditive C] →
          [inst_3 : CategoryTheory.Limits.HasBinaryBiproducts C] →
            [inst_4 : CategoryTheory.Preadditive D] →
              [inst_5 : CategoryTheory.Limits.HasBinaryBiproducts D] →
                {K L : CochainComplex C ℤ} →
                  (φ : K ⟶ L) →
                    (G : CategoryTheory.Functor C D) →
                      [inst_6 : G.Additive] →
                        (G.mapHomologicalComplex (ComplexShape.up ℤ)).mapTriangle.obj
                            (CochainComplex.mappingCone.triangle φ) ≅
                          CochainComplex.mappingCone.triangle ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.filterMap.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match some b with
    | none => h_1 ()
    | some b => h_2 b) =
    h_2 b
-- Mathlib.Data.Countable.Basic
Sum.uncountable_inr : ∀ {α : Type u} {β : Type v} [Uncountable β], Uncountable (α ⊕ β)
-- Mathlib.Topology.VectorBundle.ContinuousAlternatingMap
Bundle.Trivialization.continuousAlternatingMap_apply : ∀ {𝕜 : Type u_1} {ι : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : Fintype ι] {B : Type u_3}
  [inst_2 : TopologicalSpace B] {F₁ : Type u_4} [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁]
  {E₁ : B → Type u_5} [inst_5 : (x : B) → AddCommGroup (E₁ x)] [inst_6 : (x : B) → Module 𝕜 (E₁ x)]
  [inst_7 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [inst_8 : (x : B) → TopologicalSpace (E₁ x)]
  [inst_9 : FiberBundle F₁ E₁] [inst_10 : VectorBundle 𝕜 F₁ E₁] {F₂ : Type u_6} [inst_11 : NormedAddCommGroup F₂]
  [inst_12 : NormedSpace 𝕜 F₂] {E₂ : B → Type u_7} [inst_13 : (x : B) → AddCommGroup (E₂ x)]
  [inst_14 : (x : B) → Module 𝕜 (E₂ x)] [inst_15 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_16 : (x : B) → TopologicalSpace (E₂ x)] [inst_17 : FiberBundle F₂ E₂] [inst_18 : VectorBundle 𝕜 F₂ E₂]
  [inst_19 : ∀ (x : B), IsTopologicalAddGroup (E₂ x)] [inst_20 : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
  {e₁ : Bundle.Trivialization F₁ Bundle.TotalSpace.proj} {e₂ : Bundle.Trivialization F₂ Bundle.TotalSpace.proj}
  [he₁ : MemTrivializationAtlas e₁] [he₂ : MemTrivializationAtlas e₂]
  (p : Bundle.TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun x => E₁ x [⋀^ι]→L[𝕜] E₂ x),
  ↑(Bundle.Trivialization.continuousAlternatingMap 𝕜 ι e₁ e₂) p =
    (p.proj,
      ((Bundle.Trivialization.continuousLinearMapAt 𝕜 e₂ p.proj).compContinuousAlternatingMap
            p.snd).compContinuousLinearMap
        (Bundle.Trivialization.symmL 𝕜 e₁ p.proj))
-- Mathlib.Order.CompleteLattice.Defs
CompleteLinearOrder.toOrd : {α : Type u_8} → [self : CompleteLinearOrder α] → Ord α
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.rank_unit : ∀ {n : Type un} {R : Type uR} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R]
  [StrongRankCondition R] (A : (Matrix n n R)ˣ), (↑A).rank = Fintype.card n
-- Mathlib.Algebra.Category.MonCat.Limits
MonCat.sectionsSubmonoid.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J MonCat),
  MonCat.sectionsSubmonoid F =
    { carrier := (F.comp (CategoryTheory.forget MonCat)).sections, mul_mem' := ⋯, one_mem' := ⋯ }
-- Lean.ParserCompiler.Attribute
Lean.ParserCompiler.CombinatorAttribute.mk.injEq : ∀ (impl : Lean.AttributeImpl) (ext : Lean.SimplePersistentEnvExtension (Lean.Name × Lean.Name) (Lean.NameMap Lean.Name))
  (impl_1 : Lean.AttributeImpl)
  (ext_1 : Lean.SimplePersistentEnvExtension (Lean.Name × Lean.Name) (Lean.NameMap Lean.Name)),
  ({ impl := impl, ext := ext } = { impl := impl_1, ext := ext_1 }) = (impl = impl_1 ∧ ext = ext_1)
-- Mathlib.Logic.Equiv.Set
Equiv.Set.univ_apply : ∀ (α : Type u_3) (self : { x // x ∈ Set.univ }), (Equiv.Set.univ α) self = ↑self
-- Mathlib.CategoryTheory.Triangulated.Generators
CategoryTheory.ObjectProperty.prop_triangEnvelope_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) (X : C), P.triangEnvelope X ↔ ∃ n, P.triangEnvelopeIter n X
-- Mathlib.FieldTheory.Separable
Polynomial.separable_prod_X_sub_C_iff' : ∀ {F : Type u} [inst : Field F] {ι : Type u_1} {f : ι → F} {s : Finset ι},
  (∏ i ∈ s, (Polynomial.X - Polynomial.C (f i))).Separable ↔ ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y
-- Mathlib.Order.SupIndep
/-- If the elements of a set are independent, then any element is disjoint from the `iSup` of some
subset of the rest.  -/
iSupIndep.disjoint_biSup : ∀ {ι : Type u_5} {α : Type u_6} [inst : CompleteLattice α] {t : ι → α},
  iSupIndep t → ∀ {x : ι} {y : Set ι}, x ∉ y → Disjoint (t x) (⨆ i ∈ y, t i)
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.apply_le_mass : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) (s : Set Ω), μ s ≤ μ.mass
-- Init.Control.Lawful.Basic
/-- The `map` implementation preserves function composition.
 -/
LawfulFunctor.comp_map : ∀ {f : Type u → Type v} {inst : Functor f} [self : LawfulFunctor f] {α β γ : Type u} (g : α → β) (h : β → γ) (x : f α),
  (h ∘ g) <$> x = h <$> g <$> x
-- Mathlib.Computability.Primrec.Basic
Nat.Primrec.right : Nat.Primrec fun n => (Nat.unpair n).2
-- Mathlib.Algebra.Category.CommAlgCat.Basic
CommAlgCat.instAlgebraObjForgetAlgHomCarrier : {R : Type u} → [inst : CommRing R] → {A : CommAlgCat R} → Algebra R ((CategoryTheory.forget (CommAlgCat R)).obj A)
-- Mathlib.Algebra.Group.Hom.Basic
OneHom.inv_comp : ∀ {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : One M] [inst_1 : One N] [inst_2 : InvOneClass P] (g : OneHom N P)
  (f : OneHom M N), g⁻¹.comp f = (g.comp f)⁻¹
-- Mathlib.Algebra.Order.Ring.Idempotent
instBooleanAlgebraSubtypeProdAndEqHMulFstSndOfNatHAdd : {R : Type u_1} → [inst : CommSemiring R] → BooleanAlgebra { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.rnDeriv_zero : ∀ {α : Type u_1} {m : MeasurableSpace α} (ν : MeasureTheory.Measure α), MeasureTheory.Measure.rnDeriv 0 ν =ᵐ[ν] 0
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKey_insertMany_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {l : List (α × β)} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.1 == b.1) = false) l →
      k ∈ List.map Prod.fst l →
        ∀ {h : k' ∈ Std.DHashMap.Const.insertMany m l}, (Std.DHashMap.Const.insertMany m l).getKey k' h = k
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.IsRestriction.antisymm : ∀ {α : Type u_1} {M M' : Matroid α}, M.IsRestriction M' → M'.IsRestriction M → M = M'
-- Mathlib.Order.Interval.Finset.Basic
Finset.inf'_Ici : ∀ {α : Type u_2} [inst : SemilatticeInf α] [inst_1 : LocallyFiniteOrderTop α] (a : α), (Finset.Ici a).inf' ⋯ id = a
-- Mathlib.Analysis.Calculus.FDeriv.Bilinear
ContinuousLinearMap.hasFDerivAt_of_bilinear : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {G' : Type u_5} [inst_7 : NormedAddCommGroup G']
  [inst_8 : NormedSpace 𝕜 G'] (B : E →L[𝕜] F →L[𝕜] G) {f : G' → E} {g : G' → F} {f' : G' →L[𝕜] E} {g' : G' →L[𝕜] F}
  {x : G'},
  HasFDerivAt f f' x →
    HasFDerivAt g g' x →
      HasFDerivAt (fun y => (B (f y)) (g y))
        (((ContinuousLinearMap.precompR G' B) (f x)) g' + ((ContinuousLinearMap.precompL G' B) f') (g x)) x
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.comp₀ : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : ι → Type u_10}
  {γ : ι → Type u_11} {mβ : (i : ι) → MeasurableSpace (β i)} {mγ : (i : ι) → MeasurableSpace (γ i)}
  {f : (i : ι) → Ω → β i},
  ProbabilityTheory.iIndepFun f μ →
    ∀ (g : (i : ι) → β i → γ i),
      (∀ (i : ι), AEMeasurable (f i) μ) →
        (∀ (i : ι), AEMeasurable (g i) (MeasureTheory.Measure.map (f i) μ)) →
          ProbabilityTheory.iIndepFun (fun i => g i ∘ f i) μ
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.S_eq_U_comp_half_mul_X : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : Invertible 2] (n : ℤ),
  Polynomial.Chebyshev.S R n = (Polynomial.Chebyshev.U R n).comp (Polynomial.C ⅟2 * Polynomial.X)
-- Mathlib.Algebra.Polynomial.Monic
Function.Injective.monic_map_iff : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {f : R →+* S},
  Function.Injective ⇑f → ∀ {p : Polynomial R}, p.Monic ↔ (Polynomial.map f p).Monic
-- Mathlib.CategoryTheory.Sites.Subsheaf
CategoryTheory.Subfunctor.isSheaf_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {F : CategoryTheory.Functor Cᵒᵖ (Type w)} (G : CategoryTheory.Subfunctor F),
  CategoryTheory.Presieve.IsSheaf J F →
    (CategoryTheory.Presieve.IsSheaf J G.toFunctor ↔
      ∀ (U : Cᵒᵖ) (s : F.obj U), G.sieveOfSection s ∈ J (Opposite.unop U) → s ∈ G.obj U)
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.comp_X_add_C_ne_zero_iff : ∀ {R : Type u} [inst : CommRing R] {p : Polynomial R} {t : R}, p.comp (Polynomial.X + Polynomial.C t) ≠ 0 ↔ p ≠ 0
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
MeasureTheory.condExp_congr_ae : ∀ {α : Type u_1} {E : Type u_3} {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → E}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E], f =ᵐ[μ] g → μ[f | m] =ᵐ[μ] μ[g | m]
-- Mathlib.Algebra.Group.TypeTags.Hom
AddMonoidHom.toMultiplicative_id : ∀ {α : Type u_3} [inst : AddZeroClass α],
  AddMonoidHom.toMultiplicative (AddMonoidHom.id α) = MonoidHom.id (Multiplicative α)
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- Submonoids of a monoid `Multiplicative A` are isomorphic to additive submonoids of `A`.  -/
Submonoid.toAddSubmonoid' : {A : Type u_4} → [inst : AddZeroClass A] → Submonoid (Multiplicative A) ≃o AddSubmonoid A
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instBEqLetValue.beq : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.LetValue pu → Lean.Compiler.LCNF.LetValue pu → Bool
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.ShiftConcatInput.bit : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} →
        {len : ℕ} → Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.ShiftConcatInput aig len → aig.Ref
-- Mathlib.Algebra.Quandle
_private.Mathlib.Algebra.Quandle.0.Rack.toEnvelGroup.mapAux.match_1.eq_2 : ∀ {R : Type u_1} (motive : Rack.PreEnvelGroup R → Sort u_2) (x : R) (h_1 : Unit → motive Rack.PreEnvelGroup.unit)
  (h_2 : (x : R) → motive (Rack.PreEnvelGroup.incl x)) (h_3 : (a b : Rack.PreEnvelGroup R) → motive (a.mul b))
  (h_4 : (a : Rack.PreEnvelGroup R) → motive a.inv),
  (match Rack.PreEnvelGroup.incl x with
    | Rack.PreEnvelGroup.unit => h_1 ()
    | Rack.PreEnvelGroup.incl x => h_2 x
    | a.mul b => h_3 a b
    | a.inv => h_4 a) =
    h_2 x
-- Mathlib.Order.UpperLower.Principal
UpperSet.Ici_inj : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, UpperSet.Ici a = UpperSet.Ici b ↔ a = b
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.alter_eq_empty_iff : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {f : Option β → Option β},
  m.alter k f = ∅ ↔ (m = ∅ ∨ m.size = 1 ∧ k ∈ m) ∧ f m[k]? = none
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
/-- Any property of scheme morphisms induced by a property of ring homomorphisms is stable
under composition with open immersions.  -/
AlgebraicGeometry.HasRingHomProperty.respects_isOpenImmersion : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
  [AlgebraicGeometry.HasRingHomProperty P Q],
  (RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] => Q) →
    P.Respects AlgebraicGeometry.IsOpenImmersion
-- Mathlib.Combinatorics.Quiver.Schreier
Quiver.SchreierGraph.equiv_apply_toVertex : ∀ (V : Type u_1) {M : Type u_2} [inst : SMul M V] {S : Type u_3} (ι : S → M) (toVertex : V),
  ((Quiver.SchreierGraph.equiv V ι) toVertex).toVertex = toVertex
-- Mathlib.Topology.EMetricSpace.BoundedVariation
eVariationOn.lowerSemicontinuous_aux : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {ι : Type u_3} {F : ι → α → E}
  {p : Filter ι} {f : α → E} {s : Set α},
  (∀ x ∈ s, Filter.Tendsto (fun i => F i x) p (nhds (f x))) →
    ∀ {v : ENNReal}, v < eVariationOn f s → ∀ᶠ (n : ι) in p, v < eVariationOn (F n) s
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.eq_top_iff' : ∀ {R : Type u} [inst : NonAssocSemiring R] (A : Subsemiring R), A = ⊤ ↔ ∀ (x : R), x ∈ A
-- Lean.Meta.Basic
/-- `isDecInst` is true if the parameter's type is of the form `Decidable ...`.
This information affects the generation of congruence theorems.
 -/
Lean.Meta.ParamInfo.isDecInst : Lean.Meta.ParamInfo → Bool
-- Aesop.Tree.TreeM
Aesop.TreeM : Type → Type
-- Mathlib.Topology.Constructions.SumProd
Homeomorph.sumEmpty_apply : ∀ (X : Type u) (Y : Type v) [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : IsEmpty Y],
  ⇑(Homeomorph.sumEmpty X Y) = Sum.elim id fun a => isEmptyElim a
-- Init.Data.List.Sublist
List.sublist_replicate_iff : ∀ {α : Type u_1} {l : List α} {m : ℕ} {a : α}, l.Sublist (List.replicate m a) ↔ ∃ n ≤ m, l = List.replicate n a
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPullback.toCommSq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z}
  {g : Y ⟶ Z}, CategoryTheory.IsPullback fst snd f g → CategoryTheory.CommSq fst snd f g
-- Mathlib.LinearAlgebra.Matrix.Reindex
Matrix.reindexRingEquiv_trans_reindexRingEquiv : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} (R : Type u_11) [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : Fintype o] [inst_3 : Mul R] [inst_4 : AddCommMonoid R] (e : m ≃ n) (e' : n ≃ o),
  (Matrix.reindexRingEquiv R e).trans (Matrix.reindexRingEquiv R e') = Matrix.reindexRingEquiv R (e.trans e')
-- Mathlib.Topology.Homeomorph.Defs
/-- Open quotient maps are preserved by precomposing with a homeomorphism.  -/
Homeomorph.isOpenQuotient_comp_iff : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (e : X ≃ₜ Y) {f : Y → Z}, IsOpenQuotientMap (f ∘ ⇑e) ↔ IsOpenQuotientMap f