mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Idempotents.FunctorExtension
CategoryTheory.Idempotents.functorExtension_obj_map : ∀ (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.IsIdempotentComplete D]
  (X : CategoryTheory.Functor C D) {X_1 Y : CategoryTheory.Idempotents.Karoubi C} (f : X_1 ⟶ Y),
  ((CategoryTheory.Idempotents.functorExtension C D).obj X).map f =
    (CategoryTheory.Idempotents.toKaroubiEquivalence D).inverse.map
      (((CategoryTheory.Idempotents.functorExtension₂ C D).obj X).map f)
-- Mathlib.Topology.UniformSpace.Ultra.Constructions
IsUltraUniformity.top : ∀ {X : Type u_1}, IsUltraUniformity X
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.homothety_one : ∀ {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [inst : CommRing k] [inst_1 : AddCommGroup V1]
  [inst_2 : AddTorsor V1 P1] [inst_3 : Module k V1] (c : P1), AffineMap.homothety c 1 = AffineMap.id k P1
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.instCharZero : ∀ {K : Type u} [inst : Field K] [CharZero K], CharZero (RatFunc K)
-- Mathlib.Geometry.Manifold.MFDeriv.FDeriv
/-- **Alias** of the reverse direction of `uniqueMDiffWithinAt_iff_uniqueDiffWithinAt`. -/
UniqueDiffWithinAt.uniqueMDiffWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {x : E}, UniqueDiffWithinAt 𝕜 s x → UniqueMDiffAt[s] x
-- Lean.Meta.Closure
Lean.Meta.Closure.ToProcessElement.newFVarId : Lean.Meta.Closure.ToProcessElement → Lean.FVarId
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.ext : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : Zero Y]
  {D₁ D₂ : Function.locallyFinsuppWithin U Y}, (∀ (a : X), D₁ a = D₂ a) → D₁ = D₂
-- Std.Time.Notation.Spec
_private.Std.Time.Notation.Spec.0.Std.Time.convertText : Std.Time.Text → Lean.MacroM (Lean.TSyntax `term)
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.equiv_snd_eq_self_of_mem_of_one_mem : ∀ {G : Type u_1} [inst : Group G] {S T : Set G} (hST : Subgroup.IsComplement S T) {g : G},
  1 ∈ S → ∀ (hg : g ∈ T), (hST.equiv g).2 = ⟨g, hg⟩
-- Mathlib.Order.Max
/-- Order without top elements.  -/
NoTopOrder : (α : Type u_3) → [LE α] → Prop
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.coe_toCompacts : ∀ {α : Type u_1} [inst : TopologicalSpace α] (s : TopologicalSpace.NonemptyCompacts α), ↑s.toCompacts = ↑s
-- Mathlib.Algebra.Lie.Weights.Killing
LieAlgebra.IsKilling.sl2SubmoduleOfRoot_eq_sup : ∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra]
  [inst_5 : LieAlgebra.IsKilling K L] [inst_6 : LieModule.IsTriangularizable K (↥H) L] [inst_7 : CharZero K]
  (α : LieModule.Weight K (↥H) L) (hα : α.IsNonZero),
  LieAlgebra.IsKilling.sl2SubmoduleOfRoot hα =
    LieModule.genWeightSpace L ⇑α ⊔ LieModule.genWeightSpace L (-⇑α) ⊔ LieAlgebra.IsKilling.corootSubmodule α
-- Mathlib.Analysis.Convex.Side
AffineSubspace.WOppSide.trans_sSameSide : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y z : P}, s.WOppSide x y → s.SSameSide y z → s.WOppSide x z
-- Mathlib.Algebra.Homology.HomologicalBicomplex
/-- Auxiliary definition for `HomologicalComplex₂.flipEquivalence`.  -/
HomologicalComplex₂.flipEquivalenceUnitIso : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {I₁ : Type u_2} →
        {I₂ : Type u_3} →
          (c₁ : ComplexShape I₁) →
            (c₂ : ComplexShape I₂) →
              CategoryTheory.Functor.id (HomologicalComplex₂ C c₁ c₂) ≅
                (HomologicalComplex₂.flipFunctor C c₁ c₂).comp (HomologicalComplex₂.flipFunctor C c₂ c₁)
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.instBEqCnstrRHS.beq : Lean.Meta.Grind.CnstrRHS → Lean.Meta.Grind.CnstrRHS → Bool
-- Mathlib.MeasureTheory.Measure.GiryMonad
MeasureTheory.Measure.join_dirac : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α), (MeasureTheory.Measure.dirac μ).join = μ
-- Mathlib.CategoryTheory.Limits.Types.Pullbacks
CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj_symm_apply_fst : ∀ {X Y S : Type v} {f : X ⟶ S} {g : Y ⟶ S} {c : CategoryTheory.Limits.PullbackCone f g}
  (hc : CategoryTheory.Limits.IsLimit c) (x : CategoryTheory.Limits.Types.PullbackObj f g),
  (CategoryTheory.ConcreteCategory.hom c.fst)
      ((CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj hc).symm x) =
    (↑x).1
-- Mathlib.RingTheory.Algebraic.Integral
instIsPushoutFractionRingMvPolynomial_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [alg : Algebra.IsAlgebraic R S] [inst_3 : IsDomain S] [inst_4 : FaithfulSMul R S] {σ : Type u_4},
  Algebra.IsPushout R S (FractionRing (MvPolynomial σ R)) (FractionRing (MvPolynomial σ S))
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.BraidedCategory.braiding_tensor_left_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y Z : C) {Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (β_ (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).inv h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Z X Y).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ X Z).inv Y)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Z Y).hom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (β_ Y Z).inv)
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv h))))
-- Mathlib.Data.Set.Image
Function.Injective.preimage_image : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Injective f → ∀ (s : Set α), f ⁻¹' f '' s = s
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
ofDual_toAdd_zero : ∀ {α : Type u_1} [inst : LinearOrderedAddCommMonoidWithTop α], OrderDual.ofDual (Multiplicative.toAdd 0) = ⊤
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.combine.injEq : ∀ (c₁ c₂ c₁_1 c₂_1 : Lean.Meta.Grind.Arith.Linear.IneqCnstr),
  (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.combine c₁ c₂ =
      Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.combine c₁_1 c₂_1) =
    (c₁ = c₁_1 ∧ c₂ = c₂_1)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roc.mem_of_mem_of_le : ∀ {α : Type u} [inst : LE α] [inst_1 : LT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α] [Std.PRange.LawfulUpwardEnumerableLT α]
  {lo lo' hi a : α}, lo ≤ lo' → (a ∈ lo'<...=hi) → a ∈ lo<...=hi
-- Mathlib.MeasureTheory.Measure.FiniteMeasureExt
/-- If the integrals of all elements of a subalgebra `A` of continuous and bounded functions with
respect to two finite measures `P, P'` coincide, then the measures coincide. In other words: If a
subalgebra separates points, it separates finite measures.  -/
MeasureTheory.ext_of_forall_mem_subalgebra_integral_eq_of_pseudoEMetric_complete_countable : ∀ {E : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] [inst_1 : MeasurableSpace E] [inst_2 : PseudoEMetricSpace E]
  [BorelSpace E] [CompleteSpace E] [SecondCountableTopology E] {P P' : MeasureTheory.Measure E}
  [MeasureTheory.IsFiniteMeasure P] [MeasureTheory.IsFiniteMeasure P']
  {A : StarSubalgebra 𝕜 (BoundedContinuousFunction E 𝕜)},
  (StarSubalgebra.map (BoundedContinuousFunction.toContinuousMapStarₐ 𝕜) A).SeparatesPoints →
    (∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P') → P = P'
-- Mathlib.Topology.MetricSpace.GromovHausdorff
/-- If there are subsets which are `ε₁`-dense and `ε₃`-dense in two spaces, and
isometric up to `ε₂`, then the Gromov-Hausdorff distance between the spaces is bounded by
`ε₁ + ε₂/2 + ε₃`.  -/
GromovHausdorff.ghDist_le_of_approx_subsets : ∀ {X : Type u} [inst : MetricSpace X] [inst_1 : CompactSpace X] [inst_2 : Nonempty X] {Y : Type v}
  [inst_3 : MetricSpace Y] [inst_4 : CompactSpace Y] [inst_5 : Nonempty Y] {s : Set X} (Φ : ↑s → Y) {ε₁ ε₂ ε₃ : ℝ},
  (∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁) →
    (∀ (x : Y), ∃ y, dist x (Φ y) ≤ ε₃) →
      (∀ (x y : ↑s), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂) → GromovHausdorff.ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃
-- Mathlib.Data.Matrix.Diagonal
Matrix.transpose_ofNat : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : AddMonoidWithOne α] (d : ℕ) [inst_2 : d.AtLeastTwo],
  (OfNat.ofNat d).transpose = OfNat.ofNat d
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.Compacts.instT2Space : ∀ {α : Type u_1} [inst : TopologicalSpace α] [T2Space α], T2Space (TopologicalSpace.Compacts α)
-- Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
DifferentiableOn.continuousAlternatingMap_apply : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F [⋀^ι]→L[𝕜] G} {g : ι → E → F} {s : Set E}
  [Finite ι],
  DifferentiableOn 𝕜 f s →
    (∀ (i : ι), DifferentiableOn 𝕜 (g i) s) → DifferentiableOn 𝕜 (fun x => (f x) fun x_1 => g x_1 x) s
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Module.FaithfullyFlat.rTensor_reflects_exact : ∀ (R : Type u) (M : Type v) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N1 : Type u_1}
  [inst_3 : AddCommGroup N1] [inst_4 : Module R N1] {N2 : Type u_2} [inst_5 : AddCommGroup N2] [inst_6 : Module R N2]
  {N3 : Type u_3} [inst_7 : AddCommGroup N3] [inst_8 : Module R N3] (l12 : N1 →ₗ[R] N2) (l23 : N2 →ₗ[R] N3)
  [fl : Module.FaithfullyFlat R M],
  Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23) → Function.Exact ⇑l12 ⇑l23
-- Mathlib.GroupTheory.GroupAction.Blocks
AddAction.isBlock_iff_pairwiseDisjoint_range_vadd : ∀ {G : Type u_1} {X : Type u_2} [inst : VAdd G X] {B : Set X},
  AddAction.IsBlock G B ↔ (Set.range fun g => g +ᵥ B).PairwiseDisjoint id
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.yonedaEvaluation_map_down : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (P Q : Cᵒᵖ × CategoryTheory.Functor Cᵒᵖ (Type v₁))
  (α : P ⟶ Q) (x : (CategoryTheory.yonedaEvaluation C).obj P),
  ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.yonedaEvaluation C).map α)) x).down =
    (CategoryTheory.ConcreteCategory.hom (α.2.app Q.1)) ((CategoryTheory.ConcreteCategory.hom (P.2.map α.1)) x.down)
-- Mathlib.Analysis.Calculus.FDeriv.Basic
/-- Converse to the mean value inequality: if `f` is differentiable at `x₀` and `C`-lipschitz
on a neighborhood of `x₀` then its derivative at `x₀` has norm bounded by `C`. This version
only assumes that `‖f x - f x₀‖ ≤ C * ‖x - x₀‖` in a neighborhood of `x`.  -/
HasFDerivAt.le_of_lip' : ∀ {𝕜 : 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] {f : E → F}
  {f' : E →L[𝕜] F} {x₀ : E},
  HasFDerivAt f f' x₀ → ∀ {C : ℝ}, 0 ≤ C → (∀ᶠ (x : E) in nhds x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖) → ‖f'‖ ≤ C
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.add_assoc : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} (X : C)
  [self : CategoryTheory.AddMonObj X],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.AddMonObj.add X)
      CategoryTheory.AddMonObj.add =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X X X).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.AddMonObj.add) CategoryTheory.AddMonObj.add)
-- Mathlib.RingTheory.Multiplicity
Int.multiplicity_natAbs : ∀ (a : ℕ) (b : ℤ), multiplicity a b.natAbs = multiplicity (↑a) b
-- Mathlib.Algebra.Homology.ShortComplex.Limits
CategoryTheory.ShortComplex.preservesMonomorphisms_π₁ : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{v_2, u_2} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Limits.WalkingCospan C],
  CategoryTheory.ShortComplex.π₁.PreservesMonomorphisms
-- Mathlib.Geometry.Manifold.Submersion
/-- A choice of chart on the domain `M` of a submersion `f` at `x`:
w.r.t. this chart and the data `h.codChart` and `h.equiv`,
`f` will look like a projection `(u, v) ↦ u` in these extended charts.
The particular chart is arbitrary, but this choice matches the witnesses given by
`h.codChart` and `h.codChart`.  -/
Manifold.IsSubmersionAt.domChart : {𝕜 : Type u_1} →
  {E'' : Type u_3} →
    {H : Type u_7} →
      {G : Type u_9} →
        {E : Type u} →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : NormedAddCommGroup E] →
              [inst_2 : NormedSpace 𝕜 E] →
                [inst_3 : NormedAddCommGroup E''] →
                  [inst_4 : NormedSpace 𝕜 E''] →
                    [inst_5 : TopologicalSpace H] →
                      [inst_6 : TopologicalSpace G] →
                        {I : ModelWithCorners 𝕜 E H} →
                          {J : ModelWithCorners 𝕜 E'' G} →
                            {M : Type u_11} →
                              {N : Type u_13} →
                                [inst_7 : TopologicalSpace M] →
                                  [inst_8 : ChartedSpace H M] →
                                    [inst_9 : TopologicalSpace N] →
                                      [inst_10 : ChartedSpace G N] →
                                        {n : WithTop ℕ∞} →
                                          {f : M → N} →
                                            {x : M} → Manifold.IsSubmersionAt I J n f x → OpenPartialHomeomorph M H
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.liftIoc_comp_apply : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] {p : 𝕜} [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  [hp : Fact (0 < p)] [inst_3 : Archimedean 𝕜] {α : Type u_3} {β : Type u_4} {f : 𝕜 → α} {g : α → β} {a : 𝕜}
  {x : AddCircle p}, AddCircle.liftIoc p a (g ∘ f) x = g (AddCircle.liftIoc p a f x)
-- Mathlib.MeasureTheory.Integral.CircleIntegral
ContinuousOn.circleIntegrable : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℂ → E} {c : ℂ} {R : ℝ},
  0 ≤ R → ContinuousOn f (Metric.sphere c R) → CircleIntegrable f c R
-- Init.MetaTypes
/-- If true (default: true), extract lets from subterms that are types.
Top-level lets are always extracted.  -/
Lean.Meta.ExtractLetsConfig.types : Lean.Meta.ExtractLetsConfig → Bool
-- Mathlib.CategoryTheory.Countable
CategoryTheory.CountableCategory.instSmallCategoryHomAsType : (α : Type u) →
  [inst : CategoryTheory.Category.{v, u} α] →
    [inst_1 : CategoryTheory.CountableCategory α] →
      CategoryTheory.SmallCategory (CategoryTheory.CountableCategory.HomAsType α)
-- Init.Prelude
/-- Converts a decidable proposition into a `Bool`.

If `p : Prop` is decidable, then `decide p : Bool` is the Boolean value
that is `true` if `p` is true and `false` if `p` is false.
 -/
Decidable.decide : (p : Prop) → [h : Decidable p] → Bool
-- Std.Http.Protocol.H1
/-- Feeds input bytes into the reader side of the machine.
 -/
Std.Http.Protocol.H1.Machine.feed : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → ByteArray → Std.Http.Protocol.H1.Machine dir
-- Mathlib.MeasureTheory.Function.UniformIntegrable
MeasureTheory.uniformIntegrable_zero_meas : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : NormedAddCommGroup β] {p : ENNReal} {f : ι → α → β}
  [inst_1 : MeasurableSpace α], MeasureTheory.UniformIntegrable f p 0
-- Init.Prelude
Nat.not_succ_le_self : ∀ (n : ℕ), ¬n.succ ≤ n
-- Mathlib.Algebra.Polynomial.Degree.Units
/-- Characterization of a unit of a polynomial ring over an integral domain `R`.
See `Polynomial.isUnit_iff_coeff_isUnit_isNilpotent` when `R` is a commutative ring.  -/
Polynomial.isUnit_iff : ∀ {R : Type u} [inst : Semiring R] [NoZeroDivisors R] {p : Polynomial R}, IsUnit p ↔ ∃ r, IsUnit r ∧ Polynomial.C r = p
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.AlgHom.compLeftContinuousBounded_apply_apply : ∀ {α : Type u} {β : Type v} {γ : Type w} (𝕜 : Type u_1) [inst : NormedField 𝕜] [inst_1 : TopologicalSpace α]
  [inst_2 : NormedRing γ] [inst_3 : NormedAlgebra 𝕜 γ] [inst_4 : NormedRing β] [inst_5 : NormedAlgebra 𝕜 β]
  (g : β →ₐ[𝕜] γ) {C : NNReal} (hg : LipschitzWith C ⇑g) (f : BoundedContinuousFunction α β) (x : α),
  ((BoundedContinuousFunction.AlgHom.compLeftContinuousBounded 𝕜 g hg) f) x = g (f x)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
CliffordAlgebra.map_comp_map : ∀ {R : Type u_1} [inst : CommRing R] {M₁ : Type u_4} {M₂ : Type u_5} {M₃ : Type u_6} [inst_1 : AddCommGroup M₁]
  [inst_2 : AddCommGroup M₂] [inst_3 : AddCommGroup M₃] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R M₃] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Q₃ : QuadraticForm R M₃} (f : Q₂ →qᵢ Q₃)
  (g : Q₁ →qᵢ Q₂), (CliffordAlgebra.map f).comp (CliffordAlgebra.map g) = CliffordAlgebra.map (f.comp g)
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.piMeasurableEquivTProd_apply : ∀ {δ' : Type u_5} {π : δ' → Type u_6} [inst : (x : δ') → MeasurableSpace (π x)] [inst_1 : DecidableEq δ'] {l : List δ'}
  (hnd : l.Nodup) (h : ∀ (i : δ'), i ∈ l), ⇑(MeasurableEquiv.piMeasurableEquivTProd hnd h) = List.TProd.mk l
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.commRing.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : CommRing R] [inst_1 : CommMonoid M],
  MonoidAlgebra.commRing = { toRing := MonoidAlgebra.ring, mul_comm := ⋯ }
-- Mathlib.Algebra.BigOperators.Fin
Equiv.equivOfIsEmpty.congr_simp : ∀ (α : Sort u_1) (β : Sort u_2) [inst : IsEmpty α] [inst_1 : IsEmpty β],
  Equiv.equivOfIsEmpty α β = Equiv.equivOfIsEmpty α β
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
ContinuousLinearMap.intervalIntegral_apply : ∀ {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {μ : MeasureTheory.Measure ℝ} [inst_2 : RCLike 𝕜] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] {a b : ℝ} {φ : ℝ → F →L[𝕜] E},
  IntervalIntegrable φ μ a b → ∀ (v : F), (∫ (x : ℝ) in a..b, φ x ∂μ) v = ∫ (x : ℝ) in a..b, (φ x) v ∂μ
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
ENNReal.log_one : ENNReal.log 1 = 0
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsQF.realize_embedding : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {M : Type u_1} [inst : L.Structure M] {N : Type u_2}
  [inst_1 : L.Structure N] {F : Type u_3} [inst_2 : FunLike F M N] [EmbeddingLike F M N] [L.StrongHomClass F M N]
  {φ : L.BoundedFormula α n},
  φ.IsQF → ∀ (f : F) {v : α → M} {xs : Fin n → M}, φ.Realize (⇑f ∘ v) (⇑f ∘ xs) ↔ φ.Realize v xs
-- Init.Data.List.BasicAux
_private.Init.Data.List.BasicAux.0.List.mapMonoMImp : {m : Type u_1 → Type u_2} → {α : Type u_1} → [Monad m] → List α → (α → m α) → m (List α)
-- Mathlib.Tactic.WithoutCDot
Lean.Elab.Term.withoutCDot.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Order.Filter.Pointwise
/-- If `φ : α →* β` then `mapMonoidHom φ` is the monoid homomorphism
`Filter α →* Filter β` induced by `map φ`.  -/
Filter.mapMonoidHom : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : MulOneClass α] →
        [inst_1 : MulOneClass β] → [inst_2 : FunLike F α β] → [MonoidHomClass F α β] → F → Filter α →* Filter β
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
/-- A measure `μ` is finite on compacts if any compact set `K` satisfies `μ K < ∞`.  -/
MeasureTheory.IsFiniteMeasureOnCompacts : {α : Type u_1} → {m0 : MeasurableSpace α} → [TopologicalSpace α] → MeasureTheory.Measure α → Prop
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.indicator_apply : ∀ {α : Type u} [inst : TopologicalSpace α] (s : Set α) (hs : IsClopen s) (x : α),
  (BoundedContinuousFunction.indicator s hs) x = s.indicator 1 x
-- Init.Data.SInt.Lemmas
ISize.mod_zero : ∀ {a : ISize}, a % 0 = a
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- `ContinuousMultilinearMap.prod` as a `LinearIsometryEquiv`.  -/
ContinuousMultilinearMap.prodL : (𝕜 : Type u) →
  {ι : Type v} →
    (E : ι → Type wE) →
      (G : Type wG) →
        (G' : Type wG') →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] →
              [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)] →
                [inst_3 : SeminormedAddCommGroup G] →
                  [inst_4 : NormedSpace 𝕜 G] →
                    [inst_5 : SeminormedAddCommGroup G'] →
                      [inst_6 : NormedSpace 𝕜 G'] →
                        [inst_7 : Fintype ι] →
                          ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G' ≃ₗᵢ[𝕜]
                            ContinuousMultilinearMap 𝕜 E (G × G')
-- Mathlib.Algebra.Module.LinearMap.Basic
LinearMap.mulRight_mul : ∀ (R : Type u_6) (A : Type u_7) [inst : Semiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] (a b : A),
  LinearMap.mulRight R (a * b) = LinearMap.mulRight R b ∘ₗ LinearMap.mulRight R a
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isEmpty_ofList : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List ((a : α) × β a)},
  (Std.DTreeMap.ofList l cmp).inner.isEmpty = l.isEmpty
-- Init.Grind.Module.Basic
/-- Negation is the left inverse of addition.  -/
Lean.Grind.AddCommGroup.neg_add_cancel : ∀ {M : Type u} [self : Lean.Grind.AddCommGroup M] (a : M), -a + a = 0
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- The orthogonal projection onto a subspace as a map from the full space to itself,
as opposed to `Submodule.orthogonalProjectionOnto`, which maps into the subtype. This
version is important as it satisfies `IsStarProjection`.  -/
Submodule.starProjection : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : InnerProductSpace 𝕜 E] → (U : Submodule 𝕜 E) → [U.HasOrthogonalProjection] → E →L[𝕜] E
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.δ_zero_cocycle_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G K : CochainComplex C ℤ} {n : ℤ} (z₁ : CochainComplex.HomComplex.Cocycle F G 0)
  (z₂ : CochainComplex.HomComplex.Cochain G K n) (m : ℤ),
  CochainComplex.HomComplex.δ n m ((↑z₁).comp z₂ ⋯) = (↑z₁).comp (CochainComplex.HomComplex.δ n m z₂) ⋯
-- Init.Data.Vector.MapIdx
_private.Init.Data.Vector.MapIdx.0.Vector.mapFinIdxM.map.match_1.eq_2 : ∀ {n : ℕ} (j : ℕ) (motive : (i : ℕ) → i + j = n → Sort u_1) (i : ℕ) (inv : i + 1 + j = n)
  (h_1 : (inv : 0 + j = n) → motive 0 inv) (h_2 : (i : ℕ) → (inv : i + 1 + j = n) → motive i.succ inv),
  (match i.succ, inv with
    | 0, inv => h_1 inv
    | i.succ, inv => h_2 i inv) =
    h_2 i inv
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.mem_mk_iff' : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (p : Submodule R M)
  (h : ∀ {x : L} {m : M}, m ∈ p.carrier → ⁅x, m⁆ ∈ p.carrier) {x : M}, x ∈ { toSubmodule := p, lie_mem := h } ↔ x ∈ p