mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.MutualInductive
/-- Extract level constraints from `v ≤ r + k` for metavariables in `v`.
`Level.imax` can repush itself onto the `LevelConstraintForPropagate` work list.
 -/
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.propagateUniversesToConstructors.extractConstraints : Lean.Level → Lean.Level → ℤ → ℕ → StateT (Lean.Elab.Command.AccLevelState✝ × Lean.LMVarIdSet) Lean.MetaM Unit
-- Mathlib.LinearAlgebra.TensorProduct.Associator
TensorProduct.assoc_tensor'' : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_5} {N : Type u_6} {Q : Type u_8} {S : Type u_9}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid Q] [inst_4 : AddCommMonoid S]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R Q] [inst_8 : Module R S],
  TensorProduct.assoc R M N (TensorProduct R Q S) =
    (TensorProduct.assoc R (TensorProduct R M N) Q S).symm ≪≫ₗ LinearEquiv.rTensor S (TensorProduct.assoc R M N Q) ≪≫ₗ
        TensorProduct.assoc R M (TensorProduct R N Q) S ≪≫ₗ
      LinearEquiv.lTensor M (TensorProduct.assoc R N Q S)
-- Mathlib.Analysis.Normed.Algebra.Spectrum
_private.Mathlib.Analysis.Normed.Algebra.Spectrum.0.AlgHom.«term↑ₐ_1» : Lean.ParserDescr
-- Mathlib.Algebra.FreeAlgebra
/-- This inductive type is used to express representatives of the free algebra.
 -/
FreeAlgebra.Pre : Type u_1 → Type u_2 → Type (max u_1 u_2)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rcc_succ_succ : ∀ {m n : ℕ}, ((m + 1)...=n + 1).toList = List.map (fun x => x + 1) (m...=n).toList
-- Mathlib.GroupTheory.OrderOfElement
zpowersEquivZPowers.eq_1 : ∀ {G : Type u_1} [inst : Group G] {x y : G} [inst_1 : Finite G] (h : orderOf x = orderOf y),
  zpowersEquivZPowers h = (finEquivZPowers ⋯).symm.trans ((finCongr h).trans (finEquivZPowers ⋯))
-- Mathlib.Probability.Kernel.Composition.CompProd
ProbabilityTheory.Kernel.compProd_restrict_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ]
  {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η] {s : Set β} (hs : MeasurableSet s),
  (κ.restrict hs).compProd η = (κ.compProd η).restrict ⋯
-- Init.Core
/-- Right identity `o` is an identity.  -/
Std.LawfulRightIdentity.right_id : ∀ {α : Sort u} {β : Sort u_1} {op : α → β → α} {o : outParam β} [self : Std.LawfulRightIdentity op o] (a : α),
  op a o = a
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.prodCongr_toAffineEquiv : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {P₃ : Type u_4} {P₄ : Type u_5} {V₁ : Type u_6} {V₂ : Type u_7}
  {V₃ : Type u_8} {V₄ : Type u_9} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁] [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂]
  [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂] [inst_9 : AddCommGroup V₃] [inst_10 : Module k V₃]
  [inst_11 : AddTorsor V₃ P₃] [inst_12 : TopologicalSpace P₃] [inst_13 : AddCommGroup V₄] [inst_14 : Module k V₄]
  [inst_15 : AddTorsor V₄ P₄] [inst_16 : TopologicalSpace P₄] (e₁ : P₁ ≃ᴬ[k] P₂) (e₂ : P₃ ≃ᴬ[k] P₄),
  ↑(e₁.prodCongr e₂) = (↑e₁).prodCongr ↑e₂
-- Mathlib.Order.Filter.AtTopBot.Group
Filter.map_inv_atBot : ∀ {G : Type u_2} [inst : CommGroup G] [inst_1 : PartialOrder G] [IsOrderedMonoid G],
  Filter.map Inv.inv Filter.atBot = Filter.atTop
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.meet_join_left : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P Q R : l}
  [∀ (a : l), Lean.Order.PreservesSup (Lean.Order.meet a)],
  Lean.Order.meet P (Lean.Order.join Q R) = Lean.Order.join (Lean.Order.meet P Q) (Lean.Order.meet P R)
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.natDegree_lt_iff_degree_lt : ∀ {R : Type u} {n : ℕ} [inst : Semiring R] {p : Polynomial R}, p ≠ 0 → (p.natDegree < n ↔ p.degree < ↑n)
-- Mathlib.Analysis.BoxIntegral.Basic
/-- If `f` is integrable on a box `I`, then it is integrable on any subbox of `I`.  -/
BoxIntegral.Integrable.to_subbox : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I J : BoxIntegral.Box ι} [inst_4 : Fintype ι]
  {l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤}
  [CompleteSpace F], BoxIntegral.Integrable I l f vol → J ≤ I → BoxIntegral.Integrable J l f vol
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.LeftHomologyMapData.neg_φK : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData}
  (γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂), γ.neg.φK = -γ.φK
-- Mathlib.Data.Nat.Digits.Defs
/-- Dividing `n` by `p^i` is like truncating the first `i` digits of `n` in base `p`.
 -/
Nat.self_div_pow_eq_ofDigits_drop : ∀ {p : ℕ} (i n : ℕ), 2 ≤ p → n / p ^ i = Nat.ofDigits p (List.drop i (p.digits n))
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the forward direction of `Asymptotics.isBigO_neg_right`. -/
Asymptotics.IsBigO.of_neg_right : ∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {f : α → E}
  {g' : α → F'} {l : Filter α}, (f =O[l] fun x => -g' x) → f =O[l] g'
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.forget_reflects_isos : (CategoryTheory.forget CommGrpCat).ReflectsIsomorphisms
-- Init.Meta.Defs
_private.Init.Meta.Defs.0.Lean.Syntax.updateFirst : {α : Type u_1} → [Inhabited α] → Array α → (α → Option α) → ℕ → Option (Array α)
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.contMDiff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {H' : Type u_6} [inst_6 : TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H}
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {M' : Type u_10} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {n : WithTop ℕ∞}
  (h : Diffeomorph I I' M M' n), ContMDiff I I' n ⇑h
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.CoGrothendieck.Hom.congr : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} {a b : F.CoGrothendieck}
  {f g : a ⟶ b} (h : f = g), f.fiber = CategoryTheory.CategoryStruct.comp g.fiber (CategoryTheory.eqToHom ⋯)
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.weierstrassPExcept_of_notMem : ∀ (L : PeriodPair), ∀ l₀ ∉ L.lattice, L.weierstrassPExcept l₀ = L.weierstrassP
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKeyD_insertIfNew_le_minKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ →
    ∀ {k : α} {v : β k} {fallback : α}, (cmp ((t.insertIfNew k v).minKeyD fallback) (t.minKeyD fallback)).isLE = true
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.some_getEntryGE_eq_getEntryGE? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k : α) (t : Std.DTreeMap.Internal.Impl α β)
  {ho : t.Ordered} {he : ∃ a ∈ t, (compare a k).isGE = true},
  some (Std.DTreeMap.Internal.Impl.getEntryGE k t ho he) = Std.DTreeMap.Internal.Impl.getEntryGE? k t
-- Mathlib.Order.GaloisConnection.Defs
GaloisInsertion.mk.sizeOf_spec : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α} [inst_2 : SizeOf α]
  [inst_3 : SizeOf β] (choice : (x : α) → u (l x) ≤ x → β) (gc : GaloisConnection l u) (le_l_u : ∀ (x : β), x ≤ l (u x))
  (choice_eq : ∀ (a : α) (h : u (l a) ≤ a), choice a h = l a),
  sizeOf { choice := choice, gc := gc, le_l_u := le_l_u, choice_eq := choice_eq } = 1
-- Mathlib.Order.Atoms
IsSimpleOrder.equivBool_symm_apply : ∀ {α : Type u_4} [inst : DecidableEq α] [inst_1 : LE α] [inst_2 : BoundedOrder α] [inst_3 : IsSimpleOrder α] (x : Bool),
  IsSimpleOrder.equivBool.symm x = Bool.casesOn x ⊥ ⊤
-- Mathlib.Algebra.RingQuot
RingQuot.instNatCast : {R : Type uR} → [inst : Semiring R] → (r : R → R → Prop) → NatCast (RingQuot r)
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.signAux3_mul_and_swap : ∀ {α : Type u} [inst : DecidableEq α] [inst_1 : Finite α] (f g : Equiv.Perm α) (s : Multiset α) (hs : ∀ (x : α), x ∈ s),
  (f * g).signAux3 hs = f.signAux3 hs * g.signAux3 hs ∧ Pairwise fun x y => (Equiv.swap x y).signAux3 hs = -1
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- A closed discrete subset of a space is a CW complex.  -/
Topology.CWComplex.OfDiscreteClosed : {X : Type u_1} → [t : TopologicalSpace X] → {D : Set X} → IsDiscrete D → IsClosed D → Topology.CWComplex D
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instNeg : {α : Type u_1} → [Neg α] → Neg αᵒᵈ
-- Init.Data.BitVec.Bitblast
BitVec.usubOverflow_eq : ∀ {w : ℕ} (x y : BitVec w), x.usubOverflow y = decide (x < y)
-- Init.Data.SInt.Lemmas
Int8.not_le : ∀ {n m : Int8}, ¬n ≤ m ↔ m < n
-- Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
/-- The Haar measure defined by any orthonormal basis of a finite-dimensional inner product space
is equal to its volume measure.  -/
OrthonormalBasis.addHaar_eq_volume : ∀ {ι : Type u_4} {F : Type u_5} [inst : Fintype ι] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace ℝ F]
  [inst_3 : FiniteDimensional ℝ F] [inst_4 : MeasurableSpace F] [inst_5 : BorelSpace F] (b : OrthonormalBasis ι ℝ F),
  b.toBasis.addHaar = MeasureTheory.volume
-- Mathlib.CategoryTheory.Monoidal.Opposite.Mon
MonObj.mopEquiv_functor_map_hom_unmop : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X Y : CategoryTheory.Mon C} (f : X ⟶ Y), ((MonObj.mopEquiv C).functor.map f).hom.unmop = f.hom
-- Mathlib.CategoryTheory.Yoneda
/-- the natural bijection `(X ⟶ Y) ≃ F.obj (op X)`.  -/
CategoryTheory.Functor.RepresentableBy.homEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {F : CategoryTheory.Functor Cᵒᵖ (Type v)} →
      {Y : C} → F.RepresentableBy Y → {X : C} → (X ⟶ Y) ≃ F.obj (Opposite.op X)
-- Init.Data.List.Basic
List.reverse_cons : ∀ {α : Type u} {a : α} {as : List α}, (a :: as).reverse = as.reverse ++ [a]
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.OplaxTrans.homCategory_id_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} (Γ : F ⟶ G) (a : B),
  (CategoryTheory.CategoryStruct.id Γ).as.app a = CategoryTheory.CategoryStruct.id (Γ.app a)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.CooperSplitPred.mk.sizeOf_spec : ∀ (left : Bool) (c₁ c₂ : Lean.Meta.Grind.Arith.Cutsat.LeCnstr) (c₃? : Option Lean.Meta.Grind.Arith.Cutsat.DvdCnstr),
  sizeOf { left := left, c₁ := c₁, c₂ := c₂, c₃? := c₃? } = 1 + sizeOf left + sizeOf c₁ + sizeOf c₂ + sizeOf c₃?
-- Mathlib.Analysis.Calculus.Deriv.Add
deriv_const_add' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} (c : F), (deriv fun x => c + f x) = deriv f
-- Mathlib.Algebra.Ring.Hom.Defs
/-- Make a ring homomorphism from an additive group homomorphism from a commutative ring to an
integral domain that commutes with self multiplication, assumes that two is nonzero and `1` is sent
to `1`.  -/
AddMonoidHom.mkRingHomOfMulSelfOfTwoNeZero : {α : Type u_2} →
  {β : Type u_3} →
    [inst : CommRing α] →
      [IsDomain α] →
        [inst_2 : CommRing β] → (f : β →+ α) → (∀ (x : β), f (x * x) = f x * f x) → 2 ≠ 0 → f 1 = 1 → β →+* α
-- Mathlib.Algebra.Category.ModuleCat.Free
/-- Given a short exact sequence `0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0` of `R`-modules and linearly independent
families `v : ι → N` and `w : ι' → P`, we get a linearly independent family `ι ⊕ ι' → M`  -/
ModuleCat.linearIndependent_shortExact : ∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} [inst : Ring R] {S : CategoryTheory.ShortComplex (ModuleCat R)},
  S.ShortExact →
    ∀ {v : ι → ↑S.X₁},
      LinearIndependent R v →
        ∀ {w : ι' → ↑S.X₃},
          LinearIndependent R w →
            LinearIndependent R
              (Sum.elim (⇑(CategoryTheory.ConcreteCategory.hom S.f) ∘ v)
                (Function.invFun (ModuleCat.Hom.hom S.g).toFun ∘ w))
-- Mathlib.Order.Hom.Lattice
/-- `InfHomClass F α β` states that `F` is a type of `⊓`-preserving morphisms.

You should extend this class when you extend `InfHom`.  -/
InfHomClass : (F : Type u_6) → (α : Type u_7) → (β : Type u_8) → [Min α] → [Min β] → [FunLike F α β] → Prop
-- Std.Http.Protocol.H1.Reader
/-- Checks if the reader has encountered an error.
 -/
Std.Http.Protocol.H1.Reader.hasFailed : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Reader dir → Bool
-- Mathlib.Analysis.LocallyConvex.Separation
RCLike.geometric_hahn_banach_of_nonempty_interior : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E]
  {s t : Set E} [inst_3 : RCLike 𝕜] [inst_4 : Module 𝕜 E] [IsScalarTower ℝ 𝕜 E] [IsTopologicalAddGroup E]
  [ContinuousSMul 𝕜 E],
  Convex ℝ s →
    Convex ℝ t →
      Disjoint (interior s) t →
        (interior s).Nonempty →
          t.Nonempty → ∃ f u, f ≠ 0 ∧ (∀ a ∈ s, RCLike.re (f a) ≤ u) ∧ ∀ b ∈ t, u ≤ RCLike.re (f b)
-- Mathlib.Topology.MetricSpace.Thickening
IsCompact.cthickening : ∀ {α : Type u_2} [inst : PseudoMetricSpace α] [ProperSpace α] {s : Set α},
  IsCompact s → ∀ {r : ℝ}, IsCompact (Metric.cthickening r s)
-- Mathlib.GroupTheory.GroupExtension.Defs
/-- The left-hand side of the diagram commutes.  -/
GroupExtension.Equiv.inl_comm : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : Group N] [inst_1 : Group E] [inst_2 : Group G]
  {S : GroupExtension N E G} {E' : Type u_4} [inst_3 : Group E'] {S' : GroupExtension N E' G} (self : S.Equiv S'),
  ⇑self.toMulEquiv ∘ ⇑S.inl = ⇑S'.inl
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.of_targetAffineLocally_of_isPullback : ∀ {P : AlgebraicGeometry.AffineTargetMorphismProperty} [P.IsLocal] {X Y UX UY : AlgebraicGeometry.Scheme}
  [inst : AlgebraicGeometry.IsAffine UY] {f : X ⟶ Y} {iY : UY ⟶ Y} [AlgebraicGeometry.IsOpenImmersion iY] {iX : UX ⟶ X}
  {f' : UX ⟶ UY}, CategoryTheory.IsPullback iX f' f iY → AlgebraicGeometry.targetAffineLocally P f → P f'
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.instIsEquivalenceObjPost : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : T) (F : CategoryTheory.Functor T D) [F.IsEquivalence], (CategoryTheory.Under.post F).IsEquivalence
-- Mathlib.CategoryTheory.GradedObject.Bifunctor
CategoryTheory.GradedObject.mapBifunctorMapMapIso_inv : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) {I : Type u_4} {J : Type u_5} {K : Type u_6}
  (p : I × J → K) {X₁ X₂ : CategoryTheory.GradedObject I C₁} {Y₁ Y₂ : CategoryTheory.GradedObject J C₂}
  [inst_3 : (((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₁).obj Y₁).HasMap p]
  [inst_4 : (((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₂).obj Y₂).HasMap p] (e : X₁ ≅ X₂) (e' : Y₁ ≅ Y₂)
  (i : K),
  (CategoryTheory.GradedObject.mapBifunctorMapMapIso F p e e').inv i =
    CategoryTheory.GradedObject.mapBifunctorMapMap F p e.inv e'.inv i
-- Mathlib.ModelTheory.Algebra.Ring.Basic
FirstOrder.ringFunc.zero : FirstOrder.ringFunc 0
-- Mathlib.MeasureTheory.Measure.Haar.Extension
TopologicalGroup.IsSES.inducedMeasure.congr_simp : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : Group A] [inst_1 : Group B] [inst_2 : Group C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] {φ φ_1 : A →* B}
  (e_φ : φ = φ_1) {ψ ψ_1 : B →* C} (e_ψ : ψ = ψ_1) (H : TopologicalGroup.IsSES φ ψ) [inst_6 : IsTopologicalGroup A]
  [inst_7 : IsTopologicalGroup B] [inst_8 : MeasurableSpace A] [inst_9 : BorelSpace A]
  (μA μA_1 : MeasureTheory.Measure A) (e_μA : μA = μA_1) [hμA : μA.IsHaarMeasure] [inst_10 : IsTopologicalGroup C]
  [inst_11 : LocallyCompactSpace B] [inst_12 : MeasurableSpace C] [inst_13 : BorelSpace C]
  (μC μC_1 : MeasureTheory.Measure C) (e_μC : μC = μC_1) [hμC : μC.IsHaarMeasure] [inst_14 : T2Space B]
  [inst_15 : MeasurableSpace B] [inst_16 : BorelSpace B], H.inducedMeasure μA μC = ⋯.inducedMeasure μA_1 μC_1
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.mulVecLin_zero : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_4} {n : Type u_5} [inst_1 : Fintype n], Matrix.mulVecLin 0 = 0
-- Init.System.IO
/-- Returns `true` if and only if it is invoked during initialization.

Programs can execute `IO` actions during an initialization phase that occurs before the `main`
function is executed. The attribute `@[init <action>]` specifies which IO action is executed to set
the value of an opaque constant.
 -/
IO.initializing : BaseIO Bool
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.opEquivOpOver_functor_map : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] (X : T) {Z Y : CategoryTheory.Under (Opposite.op X)}
  (f : Z ⟶ Y),
  (CategoryTheory.Under.opEquivOpOver X).functor.map f =
    Opposite.op (CategoryTheory.Over.homMk (CategoryTheory.Under.Hom.right f).unop ⋯)
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `monovary_neg`. -/
Monovary.of_neg : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] {f : ι → α} {g : ι → β},
  Monovary (-f) (-g) → Monovary f g
-- Mathlib.Tactic.Ring.Common
/-- Cast `ExProdNat` to `ExProd btℕ sℕ`.  -/
Mathlib.Tactic.Ring.Common.ExProdNat.toExProd : (e : Q(ℕ)) →
  Mathlib.Tactic.Ring.Common.ExProdNat e →
    (e' : Q(ℕ)) × Mathlib.Tactic.Ring.Common.ExProd Mathlib.Tactic.Ring.Common.btℕ Mathlib.Tactic.Ring.Common.sℕ e'
-- Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
modularCyclotomicCharacter.pow_dvd_aux_pow_sub_aux_pow : ∀ {L : Type u} [inst : CommRing L] [inst_1 : IsDomain L] (g : L ≃+* L) (p : ℕ) [inst_2 : Fact (Nat.Prime p)]
  [∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)] {i k : ℕ},
  k ≤ i → ↑p ^ k ∣ modularCyclotomicCharacter.aux g (p ^ i) - modularCyclotomicCharacter.aux g (p ^ k)
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- **Alias** of `CategoryTheory.HasSubobjectClassifier.reflectsIsomorphismsOp`.

---

If the source of a faithful functor is the opposite category of one with a subobject classifier,
the same holds -- the functor reflects isomorphisms.
 -/
CategoryTheory.HasClassifier.reflectsIsomorphismsOp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.HasSubobjectClassifier C] (D : Type u₀)
  [inst_2 : CategoryTheory.Category.{v₀, u₀} D] (F : CategoryTheory.Functor Cᵒᵖ D) [F.Faithful], F.ReflectsIsomorphisms
-- Mathlib.Data.TypeVec
_private.Mathlib.Data.TypeVec.0.TypeVec.const.match_1.eq_2 : ∀ (motive : (x : ℕ) → TypeVec.{u_1} x → Fin2 x → Sort u_2) (n : ℕ) (x : TypeVec.{u_1} n.succ)
  (h_1 : (n : ℕ) → (α : TypeVec.{u_1} n.succ) → (a : Fin2 n) → motive n.succ α a.fs)
  (h_2 : (n : ℕ) → (x : TypeVec.{u_1} n.succ) → motive n.succ x Fin2.fz),
  (match n.succ, x, Fin2.fz with
    | n.succ, α, a.fs => h_1 n α a
    | n.succ, x, Fin2.fz => h_2 n x) =
    h_2 n x
-- Init.Data.UInt.Lemmas
UInt32.zero_def : 0 = { toBitVec := 0 }
-- Mathlib.Combinatorics.Matroid.Dual
Matroid.IsBase.compl_inter_isBasis_of_inter_isBasis : ∀ {α : Type u_1} {M : Matroid α} {B X : Set α},
  M.IsBase B → M.IsBasis (B ∩ X) X → M✶.IsBasis (M.E \ B ∩ (M.E \ X)) (M.E \ X)
-- Mathlib.Order.Atoms
instIsStronglyCoatomicOfWellFoundedGT : ∀ {α : Type u_2} [inst : PartialOrder α] [WellFoundedGT α], IsStronglyCoatomic α
-- Mathlib.Data.Finset.Lattice.Basic
Finset.inter_eq_inter_iff_left : ∀ {α : Type u_1} [inst : DecidableEq α] {s t u : Finset α}, s ∩ t = s ∩ u ↔ s ∩ u ⊆ t ∧ s ∩ t ⊆ u
-- Lean.Syntax
Lean.Syntax.Traverser.mk.injEq : ∀ (cur : Lean.Syntax) (parents : Array Lean.Syntax) (idxs : Array ℕ) (cur_1 : Lean.Syntax)
  (parents_1 : Array Lean.Syntax) (idxs_1 : Array ℕ),
  ({ cur := cur, parents := parents, idxs := idxs } = { cur := cur_1, parents := parents_1, idxs := idxs_1 }) =
    (cur = cur_1 ∧ parents = parents_1 ∧ idxs = idxs_1)
-- Mathlib.RingTheory.AdicCompletion.Exactness
/-- `AdicCompletion` over a Noetherian ring is exact on finitely generated modules.  -/
AdicCompletion.map_exact : ∀ {R : Type u} [inst : CommRing R] {I : Ideal R} {M : Type u} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : Type u} [inst_5 : AddCommGroup P]
  [inst_6 : Module R P] [IsNoetherianRing R] [Module.Finite R N] {f : M →ₗ[R] N} {g : N →ₗ[R] P},
  Function.Injective ⇑f →
    Function.Exact ⇑f ⇑g → Function.Surjective ⇑g → Function.Exact ⇑(AdicCompletion.map I f) ⇑(AdicCompletion.map I g)
-- Mathlib.Topology.Sets.Opens
toContinuousMap.congr_simp : ∀ {F : Type u_1} {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : FunLike F X Y] [inst_3 : ContinuousMapClass F X Y] (f f_1 : F), f = f_1 → ↑f = ↑f_1
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.algebraMap_def : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_7} [inst : CommMonoid M] [inst_1 : CommSemiring R] [inst_2 : CommSemiring S]
  [inst_3 : Algebra R S],
  algebraMap (MonoidAlgebra R M) (MonoidAlgebra S M) = MonoidAlgebra.mapRingHom M (algebraMap R S)
-- Mathlib.Algebra.MvPolynomial.Variables
/-- If `f₁` and `f₂` are ring homs out of the polynomial ring and `p₁` and `p₂` are polynomials,
then `f₁ p₁ = f₂ p₂` if `p₁ = p₂` and `f₁` and `f₂` are equal on `R` and on the variables
of `p₁`.  -/
MvPolynomial.hom_congr_vars : ∀ {R : Type u} {S : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  {f₁ f₂ : MvPolynomial σ R →+* S} {p₁ p₂ : MvPolynomial σ R},
  f₁.comp MvPolynomial.C = f₂.comp MvPolynomial.C →
    (∀ i ∈ p₁.vars, i ∈ p₂.vars → f₁ (MvPolynomial.X i) = f₂ (MvPolynomial.X i)) → p₁ = p₂ → f₁ p₁ = f₂ p₂
-- Mathlib.Algebra.Order.Hom.Monoid
/-- The identity map as an ordered monoid homomorphism.  -/
OrderMonoidHom.id : (α : Type u_2) → [inst : Preorder α] → [inst_1 : MulOneClass α] → α →*o α
-- Mathlib.Topology.MetricSpace.Gluing
Metric.Sigma.dist_same : ∀ {ι : Type u_1} {E : ι → Type u_2} [inst : (i : ι) → MetricSpace (E i)] (i : ι) (x y : E i),
  dist ⟨i, x⟩ ⟨i, y⟩ = dist x y
-- Mathlib.Tactic.Determinant.Bird.Cert
/-- Certify `a.subject * b.subject` from certificates for `a` and `b`.  -/
Mathlib.Tactic.Determinant.certMul : {u : Lean.Level} →
  {α : Q(Type u)} →
    {rα : Q(CommRing «$α»)} →
      Mathlib.Tactic.Determinant.Cert rα →
        Mathlib.Tactic.Determinant.Cert rα → Mathlib.Tactic.Determinant.CertM rα (Mathlib.Tactic.Determinant.Cert rα)
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
HurwitzZeta.differentiable_completedSinZeta : ∀ (a : UnitAddCircle), Differentiable ℂ (HurwitzZeta.completedSinZeta a)
-- Mathlib.Algebra.DualQuaternion
Quaternion.imJ_snd_dualNumberEquiv : ∀ {R : Type u_1} [inst : CommRing R] (q : Quaternion (DualNumber R)),
  (TrivSqZeroExt.snd (Quaternion.dualNumberEquiv q)).imJ = TrivSqZeroExt.snd q.imJ
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
Std.Iterators.Types.Flatten.IsPlausibleStep.innerSkip_flatMap : ∀ {α β α₂ γ : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α m β]
  [inst_3 : Std.Iterator α₂ m γ] {f : β → Std.IterM m γ} {it₁ : Std.IterM m β} {it₂ it₂' : Std.IterM m γ},
  it₂.IsPlausibleStep (Std.IterStep.skip it₂') →
    (Std.IterM.flatMapAfter f it₁ (some it₂)).IsPlausibleStep
      (Std.IterStep.skip (Std.IterM.flatMapAfter f it₁ (some it₂')))