mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Model
/-- Induction principle on `Impl` with an additional case split on `k ky` for
`Impl.inner _ ky _ _ _` and a generalization built in for convenience.
 -/
Std.DTreeMap.Internal.Impl.tree_split_ind : ∀ {α : Type u} {β : α → Type v} {γ : Sort w} [Ord α] (k : α → Ordering)
  {motive : Std.DTreeMap.Internal.Impl α β → γ → Prop},
  (∀ (x : γ), motive Std.DTreeMap.Internal.Impl.leaf x) →
    (∀ (n : ℕ) (ky : α) (y : β ky) (l r : Std.DTreeMap.Internal.Impl α β),
        k ky = Ordering.lt →
          (∀ (x : γ), motive l x) → ∀ (x : γ), motive (Std.DTreeMap.Internal.Impl.inner n ky y l r) x) →
      (∀ (n : ℕ) (ky : α) (y : β ky) (l r : Std.DTreeMap.Internal.Impl α β),
          k ky = Ordering.eq →
            (∀ (x : γ), motive l x) →
              (∀ (x : γ), motive r x) → ∀ (x : γ), motive (Std.DTreeMap.Internal.Impl.inner n ky y l r) x) →
        (∀ (n : ℕ) (ky : α) (y : β ky) (l r : Std.DTreeMap.Internal.Impl α β),
            k ky = Ordering.gt →
              (∀ (x : γ), motive r x) → ∀ (x : γ), motive (Std.DTreeMap.Internal.Impl.inner n ky y l r) x) →
          ∀ (t : Std.DTreeMap.Internal.Impl α β) (x : γ), motive t x
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.objMk_apply : ∀ {n m : ℕ} (f : Fin (m + 1) →o Fin (n + 1)) (i : Fin (m + 1)), (SSet.stdSimplex.objMk f) i = f i
-- Mathlib.Algebra.Category.ModuleCat.Basic
/-- linear equivalences between `Module`s are the same as (isomorphic to) isomorphisms
in `ModuleCat`  -/
linearEquivIsoModuleIso : {R : Type u} →
  [inst : Ring R] →
    {X Y : Type u} →
      [inst_1 : AddCommGroup X] →
        [inst_2 : AddCommGroup Y] →
          [inst_3 : Module R X] → [inst_4 : Module R Y] → (X ≃ₗ[R] Y) ≅ ModuleCat.of R X ≅ ModuleCat.of R Y
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
CategoryTheory.Limits.initial.mono_from : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasInitial C]
  [CategoryTheory.Limits.InitialMonoClass C] (X : C) (f : ⊥_ C ⟶ X), CategoryTheory.Mono f
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.GrpObj.inv_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G H X : C} [inst_2 : CategoryTheory.GrpObj G] [inst_3 : CategoryTheory.GrpObj H] (f : X ⟶ G) (g : G ⟶ H)
  [CategoryTheory.IsMonHom g] {Z : C} (h : H ⟶ Z),
  CategoryTheory.CategoryStruct.comp f⁻¹ (CategoryTheory.CategoryStruct.comp g h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g)⁻¹ h
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.limitCurrySwapCompLimIsoLimitCurryCompLim_hom_π_π : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  (G : CategoryTheory.Functor (J × K) C) [inst_3 : CategoryTheory.Limits.HasLimitsOfShape K C]
  [inst_4 : CategoryTheory.Limits.HasLimitsOfShape J C]
  [inst_5 : CategoryTheory.Limits.HasLimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.lim)]
  {j : J} {k : K},
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitCurrySwapCompLimIsoLimitCurryCompLim G).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.lim) j)
        (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj G).obj j) k)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.limit.π
        ((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp G)).comp CategoryTheory.Limits.lim) k)
      (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp G)).obj k)
        j)
-- Init.Data.Int.DivMod.Lemmas
Int.ext_ediv_emod : ∀ {n a b : ℤ}, a / n = b / n → a % n = b % n → a = b
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
min_le_max_of_mul_le_mul : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : LinearOrder α] {a b c d : α} [MulLeftStrictMono α] [MulRightStrictMono α],
  a * b ≤ c * d → min a b ≤ max c d
-- Lean.Message
Lean.MessageData.instCoeListExpr : Coe (List Lean.Expr) Lean.MessageData
-- Mathlib.GroupTheory.Exponent
/-- **Alias** of the reverse direction of `AddMonoid.exponent_dvd_iff_forall_nsmul_eq_zero`. -/
AddMonoid.exponent_dvd_of_forall_nsmul_eq_zero : ∀ {G : Type u} [inst : AddMonoid G] {n : ℕ}, (∀ (g : G), n • g = 0) → AddMonoid.exponent G ∣ n
-- Mathlib.Order.BooleanAlgebra.Set
Set.sdiff_nonempty : ∀ {α : Type u_1} {s t : Set α}, (s \ t).Nonempty ↔ ¬s ⊆ t
-- Mathlib.Order.CompleteLattice.Basic
biInf_prod : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CompleteLattice α] {f : β × γ → α} {s : Set β} {t : Set γ},
  ⨅ x ∈ s ×ˢ t, f x = ⨅ a ∈ s, ⨅ b ∈ t, f (a, b)
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.snd_intCast : ∀ {R : Type u} {M : Type v} [inst : AddGroupWithOne R] [inst_1 : AddGroup M] (z : ℤ), (↑z).snd = 0
-- Mathlib.FieldTheory.Finite.Basic
FiniteField.coe_frobeniusAlgHom : ∀ (K : Type u_1) (R : Type u_2) [inst : Field K] [inst_1 : Fintype K] [inst_2 : CommRing R] [inst_3 : Algebra K R],
  ⇑(FiniteField.frobeniusAlgHom K R) = fun x => x ^ Fintype.card K
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.C_mul : ∀ {R : Type u} {σ : Type u_1} {a a' : R} [inst : CommSemiring R],
  MvPolynomial.C (a * a') = MvPolynomial.C a * MvPolynomial.C a'
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
UniqueFactorizationMonoid.normalizedFactors_prod_eq_self_of_subset : ∀ {α : Type u_2} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] [inst_2 : Subsingleton αˣ] {a : α}
  {m : Multiset α},
  m ⊆ UniqueFactorizationMonoid.normalizedFactors a → UniqueFactorizationMonoid.normalizedFactors m.prod = m
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
AlgebraicTopology.DoldKan.Γ₀.obj_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] (K : ChainComplex C ℕ) (Δ : SimplexCategoryᵒᵖ),
  (AlgebraicTopology.DoldKan.Γ₀.obj K).obj Δ = AlgebraicTopology.DoldKan.Γ₀.Obj.obj₂ K Δ
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.alter.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (l' : Std.DTreeMap.Internal.Impl α β)
  (motive : Std.DTreeMap.Internal.Impl.SizedBalancedTree α β (l'.size - 1) (l'.size + 1) → Sort u_3)
  (d : Std.DTreeMap.Internal.Impl α β) (hd : d.Balanced) (hd'₁ : l'.size - 1 ≤ d.size) (hd'₂ : d.size ≤ l'.size + 1)
  (h_1 :
    (d : Std.DTreeMap.Internal.Impl α β) →
      (hd : d.Balanced) →
        (hd'₁ : l'.size - 1 ≤ d.size) →
          (hd'₂ : d.size ≤ l'.size + 1) →
            motive { impl := d, balanced_impl := hd, lb_le_size_impl := hd'₁, size_impl_le_ub := hd'₂ }),
  (match { impl := d, balanced_impl := hd, lb_le_size_impl := hd'₁, size_impl_le_ub := hd'₂ } with
    | { impl := d, balanced_impl := hd, lb_le_size_impl := hd'₁, size_impl_le_ub := hd'₂ } => h_1 d hd hd'₁ hd'₂) =
    h_1 d hd hd'₁ hd'₂
-- Mathlib.Algebra.Torsor.Defs
/-- Subtracting the result of adding a group element produces the same result
as subtracting the points and subtracting that group element.  -/
vsub_vadd_eq_vsub_sub : ∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] (p₁ p₂ : P) (g : G),
  p₁ -ᵥ (g +ᵥ p₂) = p₁ -ᵥ p₂ - g
-- Lean.Meta.Tactic.Ext
Lean.Meta.Ext.ExtTheorems.mk : Lean.Meta.DiscrTree Lean.Meta.Ext.ExtTheorem → Lean.PHashSet Lean.Name → Lean.Meta.Ext.ExtTheorems
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.full_objs : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (D : Set C), (CategoryTheory.Subgroupoid.full D).objs = D
-- Batteries.Data.Fin.Coding
/-- Encode `Bool` into `Fin 2`.  -/
Fin.encodeBool : Bool → Fin 2
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineEquiv.span_eq_top_iff : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : AddCommGroup V₂]
  [inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] {s : Set P₁} (e : P₁ ≃ᵃ[k] P₂),
  affineSpan k s = ⊤ ↔ affineSpan k (⇑e '' s) = ⊤
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.Hom.ext_iff : ∀ {C D : CategoryTheory.Cat} {x y : C.Hom D}, x = y ↔ x.toFunctor = y.toFunctor
-- Mathlib.Algebra.Group.Action.Basic
MulAction.surjective : ∀ {α : Type u_5} {β : Type u_6} [inst : Group α] [inst_1 : MulAction α β] (g : α), Function.Surjective fun x => g • x
-- Mathlib.Data.Int.Cast.Defs
/-- Default value for `IntCast.intCast` in an `AddGroupWithOne`.  -/
Int.castDef : {R : Type u} → [NatCast R] → [Neg R] → ℤ → R
-- Mathlib.Order.Directed
directed_id_iff : ∀ {α : Type u_1} {r : α → α → Prop}, Directed r id ↔ IsDirected α r
-- Mathlib.Algebra.Order.Interval.Set.SuccPred
Set.Iio_add_one_eq_Iic_of_not_isMax : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : Add α] [SuccAddOrder α] {b : α},
  ¬IsMax b → Set.Iio (b + 1) = Set.Iic b
-- Mathlib.Topology.Constructions
IsOpen.image_val : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {t : Set ↑s}, IsOpen t → ∃ c, IsOpen c ∧ Subtype.val '' t = c ∩ s
-- Batteries.Recycling.MonadSatisfying.Vector
Vector.mapFinIdxM_mk : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β : Type u_1} [inst : Monad m] [inst_1 : LawfulMonad m]
  [inst_2 : MonadSatisfying m] (a : Array α) (h : a.size = n) (f : (i : ℕ) → α → i < n → m β),
  (Vector.mk a h).mapFinIdxM f =
    (fun x =>
        match x with
        | ⟨a_1, h'⟩ => Vector.mk a_1 ⋯) <$>
      satisfying ⋯
-- Mathlib.Order.Category.FinBoolAlg
FinBoolAlg.hasForgetToFinPartOrd_forget₂_map : ∀ {X Y : FinBoolAlg} (f : X ⟶ Y),
  CategoryTheory.HasForget₂.forget₂.map f =
    CategoryTheory.InducedCategory.homMk (PartOrd.ofHom ↑(BoolAlg.Hom.hom f.hom))
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.skipSuffix?_copy : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat]
  [inst_1 : String.Slice.Pattern.Model.PatternModel pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s : String.Slice}, s.copy.skipSuffix? pat = Option.map String.Slice.Pos.copy (s.skipSuffix? pat)
-- Mathlib.CategoryTheory.GuitartExact.Basic
CategoryTheory.TwoSquare.structuredArrowDownwards_obj : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B) (X₂ : C₂)
  (X : CategoryTheory.StructuredArrow X₂ T),
  (w.structuredArrowDownwards X₂).obj X =
    (CategoryTheory.StructuredArrow.pre (R.obj X₂) L B).obj
      ((CategoryTheory.Comma.mapRight (CategoryTheory.Functor.fromPUnit (R.obj X₂)) w).obj
        (CategoryTheory.StructuredArrow.mk (R.map X.hom)))
-- Mathlib.Topology.ContinuousMap.StoneWeierstrass
ContinuousMap.sublattice_closure_eq_top : ∀ {X : Type u_1} [inst : TopologicalSpace X] [CompactSpace X] (L : Set C(X, ℝ)),
  L.Nonempty → (∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L) → (∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L) → L.SeparatesPointsStrongly → closure L = ⊤
-- Init.Data.String.Lemmas.FindPos
String.Pos.prev_lt : ∀ {s : String} {p : s.Pos} {h : p ≠ s.startPos}, p.prev h < p
-- Mathlib.Order.Hom.CompleteLattice
CompleteLatticeHom.dual_symm_apply_toFun : ∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : CompleteLatticeHom αᵒᵈ βᵒᵈ)
  (a : αᵒᵈᵒᵈ), (CompleteLatticeHom.dual.symm f) a = OrderDual.toDual (f (OrderDual.ofDual a))
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
instNonemptyUniformFun : ∀ {α : Type u_1} {β : Type u_2} [Nonempty β], Nonempty (UniformFun α β)
-- Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
ProbabilityTheory.IsGaussianProcess.shift : ∀ {T : Type u_2} {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : T → Ω → E}
  [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [BorelSpace E] [inst_3 : NormedSpace ℝ E]
  [SecondCountableTopology E] [inst_5 : Add T],
  ProbabilityTheory.IsGaussianProcess X P →
    ∀ (t₀ : T), ProbabilityTheory.IsGaussianProcess (fun t ω => X (t₀ + t) ω - X t₀ ω) P
-- Mathlib.NumberTheory.Ostrowski
/-- Given `m, n ≥ 2` and `f m = m ^ s`, `f n = n ^ t` for `s, t > 0`, we have `t ≤ s`.  -/
_private.Mathlib.NumberTheory.Ostrowski.0.Rat.AbsoluteValue.le_of_eq_pow : ∀ {f : AbsoluteValue ℚ ℝ} {m n : ℕ},
  1 < m → 1 < n → (¬∀ (n : ℕ), f ↑n ≤ 1) → ∀ {s t : ℝ}, f ↑m = ↑m ^ s → f ↑n = ↑n ^ t → t ≤ s
-- Mathlib.Topology.Order.LeftRightLim
Monotone.leftLim_le_rightLim : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
  [inst_2 : TopologicalSpace β] [OrderTopology β] {f : α → β},
  Monotone f → ∀ {x y : α}, x ≤ y → Function.leftLim f x ≤ Function.rightLim f y
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.ofSuppBddBelow_coeff : ∀ {Γ : Type u_1} {R : Type u_3} [inst : Zero R] [inst_1 : LinearOrder Γ] [inst_2 : LocallyFiniteOrder Γ] (f : Γ → R)
  (hf : BddBelow (Function.support f)) (a : Γ), (HahnSeries.ofSuppBddBelow f hf).coeff a = f a
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
/-- Continuous multilinear maps over the ring `R`, from `∀ i, M₁ i` to `M₂` where `M₁ i` and `M₂`
are modules over `R` with a topological structure. In applications, there will be compatibility
conditions between the algebraic and the topological structures, but this is not needed for the
definition.  -/
ContinuousMultilinearMap : (R : Type u) →
  {ι : Type v} →
    (M₁ : ι → Type w₁) →
      (M₂ : Type w₂) →
        [inst : Semiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
            [inst_2 : AddCommMonoid M₂] →
              [(i : ι) → Module R (M₁ i)] →
                [Module R M₂] → [(i : ι) → TopologicalSpace (M₁ i)] → [TopologicalSpace M₂] → Type (max (max v w₁) w₂)
-- Mathlib.Algebra.Group.Action.Pretransitive
/-- There is `g` such that `g • x = y`.  -/
MulAction.IsPretransitive.exists_smul_eq : ∀ {M : Type u_5} {α : Type u_6} {inst : SMul M α} [self : MulAction.IsPretransitive M α] (x y : α), ∃ g, g • x = y
-- Mathlib.RepresentationTheory.FiniteIndex
Rep.coindToInd_of_support_subset_orbit : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Group G] {S : Subgroup G} {A : Rep.{w, u, v} k ↥S}
  [inst_2 : S.FiniteIndex] (g : G) (f : ↑(Rep.coind.{u, v, v, w} S.subtype A)),
  Function.support ↑f ⊆ MulAction.orbit (↥S) g → A.coindToInd f = (Representation.IndV.mk S.subtype A.ρ g) (↑f g)
-- Init.Data.BitVec.Lemmas
BitVec.extractLsb'_cons : ∀ {w : ℕ} {y : Bool} {x : BitVec w}, BitVec.extractLsb' 0 w (BitVec.cons y x) = x
-- Init.Data.SInt.Bitwise
instAssociativeISizeHAnd : Std.Associative fun x1 x2 => x1 &&& x2
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.isMultiplicative_pow : ∀ {k : ℕ}, (ArithmeticFunction.pow k).IsMultiplicative
-- Mathlib.Logic.Equiv.Defs
Equiv.cast_apply : ∀ {α β : Sort u_1} (h : α = β) (x : α), (Equiv.cast h) x = cast h x
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.toContinuousLinearEquiv_symm : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂), ↑e.symm = (↑e).symm
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.MutualMeasure.func.injEq : ∀ (a a_1 : ℕ), (Lean.Elab.WF.GuessLex.MutualMeasure.func a = Lean.Elab.WF.GuessLex.MutualMeasure.func a_1) = (a = a_1)
-- Mathlib.CategoryTheory.Endomorphism
CategoryTheory.Functor.FullyFaithful.autMulEquivOfFullyFaithful_symm_apply_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} (hf : f.FullyFaithful) (X : C) (e : f.obj X ≅ f.obj X),
  ((hf.autMulEquivOfFullyFaithful X).symm e).inv = hf.preimage e.inv
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.opNNNorm_prod : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {G : Type wG} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [inst_7 : Fintype ι]
  (f : E [⋀^ι]→L[𝕜] F) (g : E [⋀^ι]→L[𝕜] G), ‖f.prod g‖₊ = max ‖f‖₊ ‖g‖₊
-- Mathlib.MeasureTheory.Measure.Haar.Basic
/-- If `K` is compact and `V` has nonempty interior, then the index `(K : V)` is well-defined,
there is a finite set `t` satisfying the desired properties.  -/
MeasureTheory.Measure.haar.index_defined : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] {K V : Set G},
  IsCompact K → (interior V).Nonempty → ∃ n, n ∈ Finset.card '' {t | K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Internal.USquash : (α : Type v) → [small : Std.Internal.Small α] → Type u
-- Mathlib.CategoryTheory.FiberedCategory.Cartesian
/-- Precomposing a Cartesian morphism with an isomorphism lifting the identity is Cartesian.  -/
CategoryTheory.Functor.IsCartesian.of_iso_comp : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsCartesian f φ] {a' : 𝒳}
  (φ' : a' ≅ a) [p.IsHomLift (CategoryTheory.CategoryStruct.id R) φ'.hom],
  p.IsCartesian f (CategoryTheory.CategoryStruct.comp φ'.hom φ)
-- Mathlib.Order.Interval.Set.OrderIso
OrderIso.IicTop.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderTop α],
  OrderIso.IicTop = { toEquiv := Equiv.subtypeUnivEquiv ⋯, map_rel_iff' := ⋯ }
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
ContinuousFunctionalCalculus.congr_simp : ∀ (R : Type u_1) (A : Type u_2) (p p_1 : A → Prop),
  p = p_1 →
    ∀ [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R] [inst_3 : IsTopologicalSemiring R]
      [inst_4 : ContinuousStar R] [inst_5 : Ring A] [inst_6 : StarRing A] [inst_7 : TopologicalSpace A]
      [inst_8 : Algebra R A], ContinuousFunctionalCalculus R A p = ContinuousFunctionalCalculus R A p_1
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.coe_sub : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : AddGroup Y]
  (D₁ D₂ : Function.locallyFinsuppWithin U Y), ⇑(D₁ - D₂) = ⇑D₁ - ⇑D₂
-- Mathlib.MeasureTheory.Measure.Map
MeasureTheory.Measure.mapₗ_eq_zero_iff : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {f : α → β}, Measurable f → ((MeasureTheory.Measure.mapₗ f) μ = 0 ↔ μ = 0)
-- Mathlib.RingTheory.Polynomial.DegreeLT
Polynomial.degreeLT.addLinearEquiv_symm_apply_inr : ∀ {R : Type u_1} [inst : Semiring R] {m n : ℕ} (Q : ↥(Polynomial.degreeLT R n)),
  ↑((Polynomial.degreeLT.addLinearEquiv R m n).symm
        ((LinearMap.inr R ↥(Polynomial.degreeLT R m) ↥(Polynomial.degreeLT R n)) Q)) =
    ↑Q * Polynomial.X ^ m
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.nextCoeff_C_mul_X_add_C : ∀ {R : Type u} [inst : Semiring R] {a : R},
  a ≠ 0 → ∀ (c : R), (Polynomial.C a * Polynomial.X + Polynomial.C c).nextCoeff = c
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.instTypeNameInteractiveMessage.unsafe_impl_2 : TypeName Lean.Widget.InteractiveMessage
-- Lean.Meta.Tactic.Grind.Arith.Linear.Util
Lean.Meta.Grind.Arith.Linear.getRingInst : Lean.Meta.Grind.Arith.Linear.LinearM Lean.Expr
-- Mathlib.RingTheory.MvPowerSeries.Restricted
MvPowerSeries.isRestricted_zero : ∀ {R : Type u_1} [inst : NormedRing R] {σ : Type u_2} (c : σ → ℝ), MvPowerSeries.IsRestricted c 0
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- Construct a context from a lean expression for a 2-morphism.  -/
Mathlib.Tactic.BicategoryLike.Context.mkContext? : {ρ : Type} → [self : Mathlib.Tactic.BicategoryLike.Context ρ] → Lean.Expr → Lean.MetaM (Option ρ)
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
CategoryTheory.OrthogonalReflection.D₂.multispanIndex_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (Z : C)
  [inst_1 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁]
  [inst_2 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂]
  [inst_3 : CategoryTheory.Limits.HasPushouts C] (d : (CategoryTheory.OrthogonalReflection.D₂.multispanShape W Z).L),
  (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z).left d = (↑d.fst).right
-- Aesop.Search.Expansion
Aesop.SafeRuleResult.regular.injEq : ∀ (result result_1 : Aesop.RuleResult),
  (Aesop.SafeRuleResult.regular result = Aesop.SafeRuleResult.regular result_1) = (result = result_1)
-- Mathlib.Order.Fin.Basic
Fin.orderHom_injective_iff : ∀ {α : Type u_2} [inst : PartialOrder α] {n : ℕ} (f : Fin (n + 1) →o α),
  Function.Injective ⇑f ↔ ∀ (i : Fin n), f i.castSucc ≠ f i.succ
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.isIso_iff : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B)
  {x y : CategoryTheory.Limits.CategoricalPullback F G} (f : x ⟶ y),
  CategoryTheory.IsIso f ↔ CategoryTheory.IsIso f.fst ∧ CategoryTheory.IsIso f.snd
-- Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
/-- Constructor for elements in `fiber`.  -/
CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiberMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] →
      {N : Type u'} →
        [inst_2 : CategoryTheory.Category.{v', u'} N] →
          {p : CategoryTheory.Functor N C} →
            [inst_3 : CategoryTheory.InitiallySmall N] →
              {U : N} →
                {X : C} → (p.obj U ⟶ X) → (CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiber p).obj X
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.mulPow_nc : Lean.Grind.CommRing.Power → Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon
-- Mathlib.Data.Nat.Choose.Basic
/-- `choose n k` is the number of `k`-element subsets in an `n`-element set. Also known as binomial
coefficients. For the fact that this is the number of `k`-element-subsets of an `n`-element
set, see `Finset.card_powersetCard`.  -/
Nat.choose : ℕ → ℕ → ℕ
-- Lean.Util.MonadCache
Lean.MonadStateCacheT.instMonadExceptOf : {α β : Type} →
  {m : Type → Type} →
    [inst : BEq α] →
      [inst_1 : Hashable α] →
        [Monad m] → (ε : Type u_1) → [MonadExceptOf ε m] → MonadExceptOf ε (Lean.MonadStateCacheT α β m)
-- Mathlib.Algebra.CharP.Basic
CharP.intCast_eq_intCast_mod : ∀ (R : Type u_1) [inst : AddGroupWithOne R] (p : ℕ) [CharP R p] {a : ℤ}, ↑a = ↑(a % ↑p)
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_congr'_enorm : ∀ {α : Type u_1} {ε : Type u_5} {ε' : Type u_6} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] [inst_2 : TopologicalSpace ε'] [inst_3 : ContinuousENorm ε']
  {f : α → ε} {g : α → ε'},
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable g μ →
      (∀ᵐ (a : α) ∂μ, ‖f a‖ₑ = ‖g a‖ₑ) → (MeasureTheory.Integrable f μ ↔ MeasureTheory.Integrable g μ)