mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.prodEquiv_apply : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} {M₃ : Type w₃} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃]
  [inst_4 : (i : ι) → Module R (M₁ i)] [inst_5 : Module R M₂] [inst_6 : Module R M₃]
  [inst_7 : (i : ι) → TopologicalSpace (M₁ i)] [inst_8 : TopologicalSpace M₂] [inst_9 : TopologicalSpace M₃]
  (f : ContinuousMultilinearMap R M₁ M₂ × ContinuousMultilinearMap R M₁ M₃),
  ContinuousMultilinearMap.prodEquiv f = f.1.prod f.2
-- Mathlib.Dynamics.SymbolicDynamics.Basic
SymbolicDynamics.FullShift.shift_apply : ∀ {A : Type u_1} {G : Type u_2} [inst : AddMonoid G] (g : G) (x : G → A) (h : G),
  SymbolicDynamics.FullShift.shift g x h = x (g + h)
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.vadd_set_subset_add : ∀ {α : Type u_2} [inst : Add α] {s t : Set α} {a : α}, a ∈ s → a +ᵥ t ⊆ s + t
-- Mathlib.NumberTheory.Padics.PadicNumbers
/-- An auxiliary lemma for manipulating sequence indices.  -/
PadicSeq.lift_index_right : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {f : PadicSeq p} (hf : ¬f ≈ 0) (v1 v2 : ℕ),
  padicNorm p (↑f (PadicSeq.stationaryPoint hf)) = padicNorm p (↑f (max v1 (max v2 (PadicSeq.stationaryPoint hf))))
-- Mathlib.Data.Finset.Dedup
List.perm_of_nodup_nodup_toFinset_eq : ∀ {α : Type u_1} [inst : DecidableEq α] {l l' : List α}, l.Nodup → l'.Nodup → l.toFinset = l'.toFinset → l.Perm l'
-- Mathlib.Order.RelIso.Basic
/-- **Alias** of the reverse direction of `wellFounded_lift₂_iff`.

---

A relation is well founded iff its lift to a quotient is.  -/
WellFounded.quotient_lift₂ : ∀ {α : Type u_1} {x : Setoid α} {r : α → α → Prop} {H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂},
  WellFounded r → WellFounded (Quotient.lift₂ r H)
-- Mathlib.CategoryTheory.Preadditive.Projective.Basic
CategoryTheory.Projective.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : C},
  (∀ {E X : C} (f : P ⟶ X) (e : E ⟶ X) [CategoryTheory.Epi e], ∃ f', CategoryTheory.CategoryStruct.comp f' e = f) →
    CategoryTheory.Projective P
-- Init.Data.Vector.Lemmas
Vector.getElem_append_left : ∀ {α : Type u_1} {n m i : ℕ} {xs : Vector α n} {ys : Vector α m} (hi : i < n), (xs ++ ys)[i] = xs[i]
-- Mathlib.RingTheory.GradedAlgebra.RingHom
GradedRingHom.ext_iff : ∀ {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [inst : Semiring A] [inst_1 : Semiring B]
  [inst_2 : SetLike σ A] [inst_3 : SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} {f g : 𝒜 →+*ᵍ ℬ}, f = g ↔ ∀ (x : A), f x = g x
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitSource.inj.injEq : ∀ (origin origin_1 : Lean.Meta.Grind.Origin),
  (Lean.Meta.Grind.SplitSource.inj origin = Lean.Meta.Grind.SplitSource.inj origin_1) = (origin = origin_1)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
/-- The multiplicity of an infinite place, that is the number of distinct complex embeddings that
define it, see `card_filter_mk_eq`.  -/
NumberField.InfinitePlace.mult : {K : Type u_1} → [inst : Field K] → NumberField.InfinitePlace K → ℕ
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
DiscreteConvolution.addConvolution.eq_1 : ∀ {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [inst : AddMonoid M]
  [inst_1 : CommSemiring S] [inst_2 : AddCommMonoid E] [inst_3 : AddCommMonoid E'] [inst_4 : AddCommMonoid F]
  [inst_5 : Module S E] [inst_6 : Module S E'] [inst_7 : Module S F] [inst_8 : TopologicalSpace F]
  (L : E →ₗ[S] E' →ₗ[S] F) (f : M → E) (g : M → E') (x : M),
  DiscreteConvolution.addConvolution L f g x = ∑' (ab : ↑(DiscreteConvolution.addFiber x)), (L (f (↑ab).1)) (g (↑ab).2)
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
/-- Pointwise unions of upper hemicontinuous maps are upper hemicontinuous.  -/
UpperHemicontinuousAt.union : ∀ {α : Type u_3} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : α → Set β} {x : α},
  UpperHemicontinuousAt f x → UpperHemicontinuousAt g x → UpperHemicontinuousAt (fun x => f x ∪ g x) x
-- Lean.Elab.Term.TermElabM
Lean.Elab.withoutModifyingStateWithInfoAndMessages : {m : Type → Type u_1} → {α : Type} → [MonadControlT Lean.Elab.TermElabM m] → [Monad m] → m α → m α
-- Mathlib.RingTheory.TensorProduct.MonoidAlgebra
MonoidAlgebra.tensorEquiv.eq_1 : ∀ (R : Type u_1) {M : Type u_2} {N : Type u_3} [inst : CommSemiring R],
  MonoidAlgebra.tensorEquiv R =
    ((TensorProduct.congr (MonoidAlgebra.coeffLinearEquiv R) (MonoidAlgebra.coeffLinearEquiv R)).trans
          (finsuppTensorFinsupp' R M N)).trans
      (MonoidAlgebra.coeffLinearEquiv R).symm
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.mul_iff_right : ∀ {α : Type u_1} {β : Type u_2} {f g : α → β} {mα : MeasurableSpace α} [inst : TopologicalSpace β]
  [inst_1 : CommGroup β] [IsTopologicalGroup β],
  MeasureTheory.StronglyMeasurable f → (MeasureTheory.StronglyMeasurable (f * g) ↔ MeasureTheory.StronglyMeasurable g)
-- Mathlib.Topology.Separation.Basic
Prod.instT0Space : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T0Space X] [T0Space Y],
  T0Space (X × Y)
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.col_map : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} (A : Matrix m n α) (f : α → β) (j : n),
  (A.map f).col j = f ∘ A.col j
-- Init.Grind.AC
Lean.Grind.AC.diseq_unsat_cert.eq_1 : ∀ (lhs rhs : Lean.Grind.AC.Seq), Lean.Grind.AC.diseq_unsat_cert lhs rhs = lhs.beq' rhs
-- Mathlib.CategoryTheory.Action.Limits
/-- `F.mapAction : Action V G ⥤ Action W G` preserves colimits of some shape `J` if
`V` has colimits of shape `J` and `F` preserves colimits of shape `J`.  -/
Action.Functor.mapActionPreservesColimitsOfShapeOfPreserves : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {W : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_2, u_3} W] (F : CategoryTheory.Functor V W) (G : Type u_4) [inst_2 : Monoid G]
  {J : Type u_5} [inst_3 : CategoryTheory.Category.{v_3, u_5} J] [CategoryTheory.Limits.PreservesColimitsOfShape J F]
  [CategoryTheory.Limits.HasColimitsOfShape J V], CategoryTheory.Limits.PreservesColimitsOfShape J (F.mapAction G)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem?_erase_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, (m.erase k)[k]? = none
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
SSet.S.IsUniquelyCodimOneFace.le : ∀ {X : SSet} {x y : X.S}, x.IsUniquelyCodimOneFace y → x ≤ y
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.cof_lift_iSup_add_one_le : ∀ {β : Type v} [Small.{u, v} β] (f : β → Ordinal.{u}),
  (Ordinal.lift.{v, u} (⨆ i, f i + 1)).cof ≤ Cardinal.lift.{u, v} (Cardinal.mk β)
-- Batteries.Data.PairingHeap
/-- `O(n log n)`. Monadic fold over the elements of a heap in increasing order,
by repeatedly pulling the minimum element out of the heap.
 -/
Batteries.PairingHeapImp.Heap.foldM : {m : Type u_1 → Type u_2} →
  {α : Type u_3} →
    {β : Type u_1} → [Monad m] → (α → α → Bool) → Batteries.PairingHeapImp.Heap α → β → (β → α → m β) → m β
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.OplaxTrans.naturality_naturality : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} (self : CategoryTheory.Oplax.OplaxTrans F G) {a b : B} {f g : a ⟶ b}
  (η : f ⟶ g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.map₂ η) (self.app b))
      (self.naturality g) =
    CategoryTheory.CategoryStruct.comp (self.naturality f)
      (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.map₂ η))
-- Init.Grind.Lemmas
Lean.Grind.or_eq_of_eq_false_left : ∀ {a b : Prop}, a = False → (a ∨ b) = b
-- Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
CategoryTheory.PreZeroHypercover.isLimit_toPreOneHypercover_type_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  [inst_1 : E.HasPullbacks] (F : CategoryTheory.Functor Cᵒᵖ (Type u_2)),
  Nonempty (CategoryTheory.Limits.IsLimit (E.toPreOneHypercover.multifork F)) ↔
    CategoryTheory.Presieve.IsSheafFor F E.presieve₀
-- Mathlib.Algebra.Group.Subsemigroup.Operations
MulHom.subsemigroupComap_apply_coe : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N) (N' : Subsemigroup N)
  (x : ↥(Subsemigroup.comap f N')), ↑((f.subsemigroupComap N') x) = f ↑x
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.Presieve.map_functorPullback_overForget : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {Y : CategoryTheory.Over X}
  (R : CategoryTheory.Presieve Y.left),
  CategoryTheory.Presieve.map (CategoryTheory.Over.forget X)
      (CategoryTheory.Presieve.functorPullback (CategoryTheory.Over.forget X) R) =
    R
-- Mathlib.Tactic.TermCongr
/-- Force the lhs and rhs to be defeq. For when `dsimp`-like congruence is necessary.
Clears the proof.  -/
Mathlib.Tactic.TermCongr.CongrResult.defeq : Mathlib.Tactic.TermCongr.CongrResult → Lean.MetaM Mathlib.Tactic.TermCongr.CongrResult
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.isEqvAux.eq_def : ∀ {α : Type u} (xs ys : Array α) (hsz : xs.size = ys.size) (p : α → α → Bool) (x : ℕ) (x_1 : x ≤ xs.size),
  xs.isEqvAux ys hsz p x x_1 =
    match x, x_1 with
    | 0, x => true
    | i.succ, h => p xs[i] ys[i] && xs.isEqvAux ys hsz p i ⋯
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- Transfer reflection of colimits along an equivalence in the shape.  -/
CategoryTheory.Limits.reflectsColimitsOfShape_of_equiv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {J' : Type w₂}
  [inst_3 : CategoryTheory.Category.{w₂', w₂} J'] (e : J ≌ J') (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.ReflectsColimitsOfShape J F], CategoryTheory.Limits.ReflectsColimitsOfShape J' F
-- Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly
CategoryTheory.JointlyReflectIsomorphisms.isIso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_4, u_1} C] {I : Type u_2} {D : I → Type u_3}
  [inst_1 : (i : I) → CategoryTheory.Category.{u_5, u_3} (D i)] {F : (i : I) → CategoryTheory.Functor C (D i)},
  CategoryTheory.JointlyReflectIsomorphisms F →
    ∀ {X Y : C} (f : X ⟶ Y) [∀ (i : I), CategoryTheory.IsIso ((F i).map f)], CategoryTheory.IsIso f
-- Std.Data.ExtDHashMap.Lemmas
_private.Std.Data.ExtDHashMap.Lemmas.0.Std.ExtDHashMap.insert.eq_1 : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m : Std.ExtDHashMap α β) (a : α) (b : β a),
  m.insert a b = Std.ExtDHashMap.lift (fun m => Std.ExtDHashMap.mk (m.insert a b)) ⋯ m
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
CategoryTheory.Monoidal.rightUnitor_hom : ∀ (C : CategoryTheory.Cat),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor C).hom =
    (CategoryTheory.Prod.fst ↑C ↑(CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Cat)).toCatHom
-- Mathlib.LinearAlgebra.Pi
/-- Linear map between the function spaces `I → M₂` and `I → M₃`, induced by a linear map `f`
between `M₂` and `M₃`.  -/
LinearMap.compLeft : {R : Type u} →
  {M₂ : Type w} →
    {M₃ : Type y} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M₂] →
          [inst_2 : Module R M₂] →
            [inst_3 : AddCommMonoid M₃] →
              [inst_4 : Module R M₃] → (M₂ →ₗ[R] M₃) → (I : Type u_1) → (I → M₂) →ₗ[R] I → M₃
-- Lean.Meta.Tactic.LibrarySearch
/-- A library search candidate using symmetry includes the goal to solve, the metavar
context for that goal, and the name and orientation of a rule to try using with goal.
 -/
Lean.Meta.LibrarySearch.Candidate : Type
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.insert!.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (v : β k),
  Std.DTreeMap.Internal.Impl.insert! k v Std.DTreeMap.Internal.Impl.leaf =
    Std.DTreeMap.Internal.Impl.inner 1 k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rii.pairwise_toList_lt : ∀ {α : Type u} {r : Std.Rii α} [inst : LT α] [inst_1 : Std.PRange.Least? α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.Rxi.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerableLeast? α],
  List.Pairwise (fun a b => a < b) r.toList
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
/-- A linear isometric equivalence between two normed vector spaces.  -/
«term_≃ₗᵢ[_]_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMap.coe_comp : ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H} {K : Type u_3} [inst_2 : Add K] {c : K}
  (g : AddConstMap H K b c) (f : AddConstMap G H a b), ⇑(g.comp f) = ⇑g ∘ ⇑f
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rco.forIn'_eq_forIn'_toList : ∀ {α : Type u} {r : Std.Rco α} [inst : LE α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerableLT α] [inst_6 : Std.Rxo.IsAlwaysFinite α]
  [inst_7 : Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [inst_8 : Monad m]
  [LawfulMonad m] {f : (a : α) → a ∈ r → γ → m (ForInStep γ)},
  forIn' r init f = forIn' r.toList init fun a ha acc => f a ⋯ acc
-- Mathlib.Topology.Algebra.Module.IsWeak
/-- Map `F` into the topological dual of `E` with the weak topology induced by `F`  -/
LinearMap.IsWeak.eval : {𝕜 : Type u_2} →
  {E : Type u_3} →
    {F : Type u_4} →
      [inst : CommSemiring 𝕜] →
        [inst_1 : TopologicalSpace 𝕜] →
          [inst_2 : AddCommMonoid E] →
            [inst_3 : Module 𝕜 E] →
              [inst_4 : AddCommMonoid F] →
                [inst_5 : Module 𝕜 F] →
                  [inst_6 : TopologicalSpace E] →
                    (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) →
                      [hB : B.IsWeak] →
                        [inst_7 : ContinuousAdd 𝕜] → [inst_8 : ContinuousConstSMul 𝕜 𝕜] → F →ₗ[𝕜] StrongDual 𝕜 E
-- Mathlib.LinearAlgebra.Multilinear.Basic
LinearMap.zero_compMultilinearMap : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} {M₃ : Type v₃} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃]
  [inst_4 : (i : ι) → Module R (M₁ i)] [inst_5 : Module R M₂] [inst_6 : Module R M₃] (f : MultilinearMap R M₁ M₂),
  LinearMap.compMultilinearMap 0 f = 0
-- Mathlib.Algebra.Order.Group.Cone
/-- Construct a partial order by designating a cone in an abelian group.  -/
PartialOrder.mkOfAddGroupCone : {S : Type u_1} →
  {G : Type u_2} → [inst : AddCommGroup G] → [inst_1 : SetLike S G] → S → [AddGroupConeClass S G] → PartialOrder G
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Sorted.below.seq : ∀
  {motive :
    {basis : Tactic.ComputeAsymptotics.Basis} →
      (a : Tactic.ComputeAsymptotics.MultiseriesExpansion basis) → a.Sorted → Prop}
  {hd : ℝ → ℝ} {tl : List (ℝ → ℝ)} (ms : Tactic.ComputeAsymptotics.MultiseriesExpansion (hd :: tl))
  (h_coef : ∀ x ∈ ms.seq, x.2.Sorted) (h_Pairwise : Stream'.Seq.Pairwise (fun x1 x2 => x1 > x2) ms.seq),
  (∀ (x : ℝ × Tactic.ComputeAsymptotics.MultiseriesExpansion tl) (a : x ∈ ms.seq),
      Tactic.ComputeAsymptotics.MultiseriesExpansion.Sorted.below ⋯) →
    (∀ (x : ℝ × Tactic.ComputeAsymptotics.MultiseriesExpansion tl) (a : x ∈ ms.seq), motive x.2 ⋯) →
      Tactic.ComputeAsymptotics.MultiseriesExpansion.Sorted.below ⋯
-- Mathlib.Topology.Separation.Hausdorff
tendsto_nhds_unique : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [T2Space X] {f : Y → X} {l : Filter Y} {a b : X} [l.NeBot],
  Filter.Tendsto f l (nhds a) → Filter.Tendsto f l (nhds b) → a = b
-- 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`.  -/
HasFDerivAt.le_of_lipschitzOn : ∀ {𝕜 : 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₀ → ∀ {s : Set E}, s ∈ nhds x₀ → ∀ {C : NNReal}, LipschitzOnWith C f s → ‖f'‖ ≤ ↑C
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.instAddCommGroupHom : {R : Type u} → [inst : Ring R] → {M N : ModuleCat R} → AddCommGroup (M ⟶ N)
-- Lean.Meta.AbstractMVars
Lean.Meta.AbstractMVars.State.mk.injEq : ∀ (ngen : Lean.NameGenerator) (lctx : Lean.LocalContext) (mctx : Lean.MetavarContext) (nextParamIdx : ℕ)
  (paramNames : Array Lean.Name) (fvars mvars : Array Lean.Expr) (lmap : Std.HashMap Lean.LMVarId Lean.Level)
  (emap : Std.HashMap Lean.MVarId Lean.Expr) (abstractLevels : Bool) (ngen_1 : Lean.NameGenerator)
  (lctx_1 : Lean.LocalContext) (mctx_1 : Lean.MetavarContext) (nextParamIdx_1 : ℕ) (paramNames_1 : Array Lean.Name)
  (fvars_1 mvars_1 : Array Lean.Expr) (lmap_1 : Std.HashMap Lean.LMVarId Lean.Level)
  (emap_1 : Std.HashMap Lean.MVarId Lean.Expr) (abstractLevels_1 : Bool),
  ({ ngen := ngen, lctx := lctx, mctx := mctx, nextParamIdx := nextParamIdx, paramNames := paramNames, fvars := fvars,
        mvars := mvars, lmap := lmap, emap := emap, abstractLevels := abstractLevels } =
      { ngen := ngen_1, lctx := lctx_1, mctx := mctx_1, nextParamIdx := nextParamIdx_1, paramNames := paramNames_1,
        fvars := fvars_1, mvars := mvars_1, lmap := lmap_1, emap := emap_1, abstractLevels := abstractLevels_1 }) =
    (ngen = ngen_1 ∧
      lctx = lctx_1 ∧
        mctx = mctx_1 ∧
          nextParamIdx = nextParamIdx_1 ∧
            paramNames = paramNames_1 ∧
              fvars = fvars_1 ∧ mvars = mvars_1 ∧ lmap = lmap_1 ∧ emap = emap_1 ∧ abstractLevels = abstractLevels_1)
-- Mathlib.Control.Bitraversable.Lemmas
Bitraversable.tfst_comp_tsnd : ∀ {t : Type u → Type u → Type u} [inst : Bitraversable t] {F G : Type u → Type u} [inst_1 : Applicative F]
  [inst_2 : Applicative G] [LawfulBitraversable t] [LawfulApplicative F] [LawfulApplicative G] {α₀ α₁ β₀ β₁ : Type u}
  (f : α₀ → F α₁) (f' : β₀ → G β₁),
  Functor.Comp.mk ∘ Functor.map (Bitraversable.tfst f) ∘ Bitraversable.tsnd f' =
    bitraverse (Functor.Comp.mk ∘ pure ∘ f) (Functor.Comp.mk ∘ Functor.map pure ∘ f')
-- Mathlib.Algebra.AddConstMap.Basic
/-- A bundled map `f : G → H` such that `f (x + a) = f x + b` for all `x`,
denoted as `f : G →+c[a, b] H`.

One can think about `f` as a lift to `G` of a map between two `AddCircle`s.  -/
AddConstMap : (G : Type u_1) → (H : Type u_2) → [Add G] → [Add H] → G → H → Type (max u_1 u_2)
-- Mathlib.Combinatorics.SimpleGraph.IncMatrix
/-- `G.incMatrix R` is the `α × Sym2 α` matrix whose `(a, e)`-entry is `1` if `e` is incident to
`a` and `0` otherwise.  -/
SimpleGraph.incMatrix : (R : Type u_1) →
  {α : Type u_2} →
    (G : SimpleGraph α) → [Zero R] → [One R] → [DecidableEq α] → [DecidableRel G.Adj] → Matrix α (Sym2 α) R
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.instMulActionClosedBall : MulAction Complex.UnitClosedDisc Complex.UnitDisc
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.DominatedFinMeasAdditive.add : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} [inst : SeminormedAddCommGroup β]
  {T T' : Set α → β} {C C' : ℝ},
  MeasureTheory.DominatedFinMeasAdditive μ T C →
    MeasureTheory.DominatedFinMeasAdditive μ T' C' → MeasureTheory.DominatedFinMeasAdditive μ (T + T') (C + C')
-- Mathlib.Logic.Function.Basic
/-- **Alias** of `Std.Symm.forall_existsUnique_iff`.

---

A symmetric relation `r : α → α → Prop` is "function-like"
(for each `a` there exists a unique `b` such that `r a b`)
if and only if it is `(f · = ·)` for some involutive function `f`.  -/
Symmetric.forall_existsUnique_iff : ∀ {α : Sort u_1} {r : α → α → Prop} [Std.Symm r],
  (∀ (a : α), ∃! b, r a b) ↔ ∃ f, Function.Involutive f ∧ ∀ {a b : α}, r a b ↔ f a = b
-- Mathlib.CategoryTheory.Sites.Descent.IsStack
/-- The property that a pseudofunctor `F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat`
has effective descent for a Grothendieck topology, i.e. is a stack.
(See the terminological note in the introduction of the file
`Mathlib/CategoryTheory/Sites/Descent/IsPrestack.lean`.)  -/
CategoryTheory.Pseudofunctor.IsStack : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat →
      CategoryTheory.GrothendieckTopology C → Prop
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj_hom_ext_iff : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A]
  {data : (X : C) → F.OneHypercoverDenseData J₀ J X} [inst_3 : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A]
  {G₀ : CategoryTheory.Sheaf J₀ A} {X : C} {Z : A}
  {f g : Z ⟶ CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj data G₀ X},
  f = g ↔
    ∀ (i : (data X).I₀),
      CategoryTheory.CategoryStruct.comp f
          (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjπ data G₀ X i) =
        CategoryTheory.CategoryStruct.comp g
          (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjπ data G₀ X i)
-- Mathlib.LinearAlgebra.Dimension.Constructions
finrank_span_set_eq_card : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  {s : Set M} [inst_4 : Fintype ↑s], LinearIndepOn R id s → Module.finrank R ↥(Submodule.span R s) = s.toFinset.card
-- Mathlib.CategoryTheory.Limits.Shapes.End
/-- Construct a morphism to the end from its universal property.  -/
CategoryTheory.Limits.Wedge.IsLimit.lift : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {C : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} C] →
        {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} →
          {c : CategoryTheory.Limits.Wedge F} →
            CategoryTheory.Limits.IsLimit c →
              {X : C} →
                (f : (j : J) → X ⟶ (F.obj (Opposite.op j)).obj j) →
                  (∀ ⦃i j : J⦄ (g : i ⟶ j),
                      CategoryTheory.CategoryStruct.comp (f i) ((F.obj (Opposite.op i)).map g) =
                        CategoryTheory.CategoryStruct.comp (f j) ((F.map g.op).app j)) →
                    (X ⟶ c.pt)
-- Init.Data.BitVec.Lemmas
/-- Characterize `x.toInt` in terms of `x.msb`.  -/
BitVec.toInt_eq_msb_cond : ∀ {w : ℕ} (x : BitVec w), x.toInt = if x.msb = true then ↑x.toNat - ↑(2 ^ w) else ↑x.toNat
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- This is the loop implementation of the default instance `IteratorLoop.defaultImplementation`.
 -/
Std.IterM.DefaultConsumers.forIn'.wf : {m : Type w → Type w'} →
  {α β : Type w} →
    [inst : Std.Iterator α m β] →
      {n : Type x → Type x'} →
        [Monad n] →
          ((γ : Type w) → (δ : Type x) → (γ → n δ) → m γ → n δ) →
            (γ : Type x) →
              (PlausibleForInStep : β → γ → ForInStep γ → Prop) →
                Std.IteratorLoop.WellFounded α m PlausibleForInStep →
                  (it : Std.IterM m β) →
                    γ →
                      (P : β → Prop) →
                        (∀ (b : β), it.IsPlausibleIndirectOutput b → P b) →
                          ((b : β) → P b → (c : γ) → n (Subtype (PlausibleForInStep b c))) → n γ
-- Init.Data.Bool
Bool.ite_eq_true_else_eq_false : ∀ {b : Bool} {q : Prop}, (if b = true then q else b = false) ↔ b = true → q