mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Convex.Cone.Dual
/-- **Alias** of `PointedCone.dual_anti`. -/
PointedCone.dual_le_dual : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {N : Type u_3} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  {p : M →ₗ[R] N →ₗ[R] R} {s t : Set M}, t ⊆ s → PointedCone.dual p s ≤ PointedCone.dual p t
-- Mathlib.Combinatorics.SimpleGraph.Sum
_private.Mathlib.Combinatorics.SimpleGraph.Sum.0.SimpleGraph.edgeSetSumEquiv.match_1.eq_2 : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W}
  (motive : (x x_1 : V ⊕ W) → (G ⊕g H).Adj x x_1 → Sort u_3) (u v : W) (h : (G ⊕g H).Adj (Sum.inr u) (Sum.inr v))
  (h_1 : (u v : V) → (h : (G ⊕g H).Adj (Sum.inl u) (Sum.inl v)) → motive (Sum.inl u) (Sum.inl v) h)
  (h_2 : (u v : W) → (h : (G ⊕g H).Adj (Sum.inr u) (Sum.inr v)) → motive (Sum.inr u) (Sum.inr v) h)
  (h_3 : (u : V) → (v : W) → (h : (G ⊕g H).Adj (Sum.inl u) (Sum.inr v)) → motive (Sum.inl u) (Sum.inr v) h)
  (h_4 : (u : W) → (v : V) → (h : (G ⊕g H).Adj (Sum.inr u) (Sum.inl v)) → motive (Sum.inr u) (Sum.inl v) h),
  (match Sum.inr u, Sum.inr v, h with
    | Sum.inl u, Sum.inl v, h => h_1 u v h
    | Sum.inr u, Sum.inr v, h => h_2 u v h
    | Sum.inl u, Sum.inr v, h => h_3 u v h
    | Sum.inr u, Sum.inl v, h => h_4 u v h) =
    h_2 u v h
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey!_insertIfNew_le_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α} {v : β}, (cmp (t.insertIfNew k v).minKey! k).isLE = true
-- Mathlib.Topology.MetricSpace.Dilation
/-- A dilation from a complete emetric space is a closed embedding  -/
Dilation.isClosedEmbedding : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : EMetricSpace α] [inst_1 : FunLike F α β] [CompleteSpace α]
  [inst_3 : EMetricSpace β] [DilationClass F α β] (f : F), Topology.IsClosedEmbedding ⇑f
-- Mathlib.LinearAlgebra.TensorProduct.Defs
TensorProduct.instInhabited : {R : Type u_1} →
  [inst : CommSemiring R] →
    (M : Type u_7) →
      (N : Type u_8) →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid N] → [inst_3 : Module R M] → [inst_4 : Module R N] → Inhabited (TensorProduct R M N)
-- Mathlib.Data.Finmap
Finmap.lookup_union_right : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {s₁ s₂ : Finmap β},
  a ∉ s₁ → Finmap.lookup a (s₁ ∪ s₂) = Finmap.lookup a s₂
-- Mathlib.Tactic.Determinant.Bird.Cert
/-- Certify an entry of `(BirdDet.stepEntry n A)^[t] (BirdDet.get n A)`.  -/
Mathlib.Tactic.Determinant.certIterStepEntry : {u : Lean.Level} →
  {α : Q(Type u)} →
    {rα : Q(CommRing «$α»)} → ℕ → ℕ → ℕ → Mathlib.Tactic.Determinant.CertM rα (Mathlib.Tactic.Determinant.Cert rα)
-- Aesop.Index
Aesop.Index.mk.inj : ∀ {α : Type} {byTarget byHyp : Lean.Meta.DiscrTree (Aesop.Rule α)} {unindexed : Lean.PHashSet (Aesop.Rule α)}
  {byTarget_1 byHyp_1 : Lean.Meta.DiscrTree (Aesop.Rule α)} {unindexed_1 : Lean.PHashSet (Aesop.Rule α)},
  { byTarget := byTarget, byHyp := byHyp, unindexed := unindexed } =
      { byTarget := byTarget_1, byHyp := byHyp_1, unindexed := unindexed_1 } →
    byTarget = byTarget_1 ∧ byHyp = byHyp_1 ∧ unindexed = unindexed_1
-- Mathlib.Data.Nat.Digits.Defs
Nat.digits_ne_nil_iff_ne_zero : ∀ {b n : ℕ}, b.digits n ≠ [] ↔ n ≠ 0
-- Mathlib.MeasureTheory.Measure.RegularityCompacts
MeasureTheory.innerRegularWRT_isCompact_isOpen : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [SecondCountableTopology α]
  [TopologicalSpace.IsCompletelyPseudoMetrizableSpace α] [OpensMeasurableSpace α] (P : MeasureTheory.Measure α)
  [MeasureTheory.IsFiniteMeasure P], P.InnerRegularWRT IsCompact IsOpen
-- Mathlib.Analysis.Normed.Operator.Basic
/-- The operator norm satisfies the triangle inequality.  -/
ContinuousLinearMap.opNorm_add_le : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f g : E →SL[σ₁₂] F),
  ‖f + g‖ ≤ ‖f‖ + ‖g‖
-- Mathlib.Combinatorics.SimpleGraph.Metric
/-- The ball of radius two consists of the center and its neighbors.  -/
SimpleGraph.ball_two : ∀ {V : Type u_1} {G : SimpleGraph V} {c : V}, G.ball c 2 = insert c (G.neighborSet c)
-- Mathlib.Analysis.SpecialFunctions.Complex.Analytic
hasFPowerSeriesAt_log_one_add : HasFPowerSeriesAt (fun x => Real.log (1 + x)) (FormalMultilinearSeries.ofScalars ℝ fun n => -(-1) ^ n / ↑n) 0
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.nsmul_right_monotone : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddMonoid α] {s : Finset α}, 0 ∈ s → Monotone fun x => x • s
-- Mathlib.Topology.Order.LocalExtr
IsLocalMin.add : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : AddCommMonoid β] [inst_2 : PartialOrder β]
  [IsOrderedAddMonoid β] {f g : α → β} {a : α}, IsLocalMin f a → IsLocalMin g a → IsLocalMin (fun x => f x + g x) a
-- Mathlib.Topology.Algebra.PontryaginDual
PontryaginDual.instFiniteOfDiscreteTopologyOfCompactSpace : ∀ {A : Type u_1} [inst : Monoid A] [inst_1 : TopologicalSpace A] [DiscreteTopology A] [CompactSpace A],
  Finite (PontryaginDual A)
-- Aesop.Script.SpecificTactics
Aesop.Script.TacticBuilder.simpAllOrSimpAtStarOnly : Bool → Lean.MVarId → Option Lean.Term → Lean.Meta.Simp.UsedSimps → Aesop.Script.TacticBuilder
-- Batteries.Tactic.Lint.Basic
/-- Returns true if `decl` is a private or automatically generated declaration.

Also returns true if `decl` is an internal name or created during macro expansion.
 -/
Lean.Environment.isPrivateOrAutoDecl : Lean.Environment → Lean.Name → Bool
-- Mathlib.LinearAlgebra.Determinant
LinearMap.detAux.congr_simp : ∀ {M : Type u_7} [inst : AddCommGroup M] {ι : Type u_8} {inst_1 : DecidableEq ι} [inst_2 : DecidableEq ι]
  [inst_3 : Fintype ι] {A : Type u_9} [inst_4 : CommRing A] [inst_5 : Module A M] (a a_1 : Trunc (Module.Basis ι A M)),
  a = a_1 → LinearMap.detAux a = LinearMap.detAux a_1
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
cmp_sub_zero : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LinearOrder α] [AddRightMono α] (a b : α), cmp (a - b) 0 = cmp a b
-- Init.Data.UInt.Lemmas
USize.toUInt8_ofBitVec : ∀ (b : BitVec System.Platform.numBits), { toBitVec := b }.toUInt8 = { toBitVec := BitVec.setWidth 8 b }
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.mem_vanishingIdeal : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] {𝒜 : ℕ → σ}
  [inst_3 : GradedRing 𝒜] (t : Set (ProjectiveSpectrum 𝒜)) (f : A),
  f ∈ ProjectiveSpectrum.vanishingIdeal t ↔ ∀ x ∈ t, f ∈ x.asHomogeneousIdeal
-- Mathlib.Analysis.Normed.Group.Hom
/-- If one controls the norm of every `f x`, then one controls the norm of `f`.  -/
NormedAddGroupHom.opNorm_le_bound : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
  (f : NormedAddGroupHom V₁ V₂) {M : ℝ}, 0 ≤ M → (∀ (x : V₁), ‖f x‖ ≤ M * ‖x‖) → ‖f‖ ≤ M
-- Mathlib.Algebra.Algebra.Basic
Module.ker_algebraMap_end : ∀ (K : Type u) (V : Type v) [inst : Semifield K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V] (a : K),
  a ≠ 0 → LinearMap.ker ((algebraMap K (Module.End K V)) a) = ⊥
-- Mathlib.Control.Traversable.Instances
List.instLawfulTraversable : LawfulTraversable List
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxc.Iterator.instIteratorLoop.loop.match_3.eq_1 : ∀ {α : Type u_1} (γ : Type u_1) (Pl : α → γ → ForInStep γ → Prop) (next : α) (acc : γ)
  (motive : Subtype (Pl next acc) → Sort u_2) (acc' : γ) (h' : Pl next acc (ForInStep.yield acc'))
  (h_1 : (acc' : γ) → (h' : Pl next acc (ForInStep.yield acc')) → motive ⟨ForInStep.yield acc', h'⟩)
  (h_2 : (acc' : γ) → (property : Pl next acc (ForInStep.done acc')) → motive ⟨ForInStep.done acc', property⟩),
  (match ⟨ForInStep.yield acc', h'⟩ with
    | ⟨ForInStep.yield acc', h'⟩ => h_1 acc' h'
    | ⟨ForInStep.done acc', property⟩ => h_2 acc' property) =
    h_1 acc' h'
-- Lean.Server.Utils
Lean.Server.instInhabitedDocumentMeta.default : Lean.Server.DocumentMeta
-- Init.Data.SInt.Lemmas
Int16.toISize_ofIntLE : ∀ {n : ℤ} (h₁ : Int16.minValue.toInt ≤ n) (h₂ : n ≤ Int16.maxValue.toInt),
  (Int16.ofIntLE n h₁ h₂).toISize = ISize.ofIntLE n ⋯ ⋯
-- Mathlib.NumberTheory.LSeries.Linearity
LSeries_neg : ∀ (f : ℕ → ℂ) (s : ℂ), LSeries (-f) s = -LSeries f s
-- Init.Data.SInt.Bitwise
Int64.toUInt64_or : ∀ (a b : Int64), (a ||| b).toUInt64 = a.toUInt64 ||| b.toUInt64
-- Mathlib.Algebra.BigOperators.Intervals
Finset.sum_Ioc_consecutive : ∀ {M : Type u_3} [inst : AddCommMonoid M] (f : ℕ → M) {m n k : ℕ},
  m ≤ n → n ≤ k → ∑ i ∈ Finset.Ioc m n, f i + ∑ i ∈ Finset.Ioc n k, f i = ∑ i ∈ Finset.Ioc m k, f i
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.map_sup : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type u_3}
  [inst_3 : Field K] [inst_4 : Algebra F K] (s t : IntermediateField F E) (f : E →ₐ[F] K),
  IntermediateField.map f (s ⊔ t) = IntermediateField.map f s ⊔ IntermediateField.map f t
-- Mathlib.Order.Category.BoolAlg
/-- `OrderDual` as a functor.  -/
BoolAlg.dual : CategoryTheory.Functor BoolAlg BoolAlg
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
neg_lt_neg_iff : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddLeftStrictMono α] {a b : α} [AddRightStrictMono α],
  -a < -b ↔ b < a
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.coe_copy : ∀ {G : Type u_1} [inst : AddGroup G] (K : AddSubgroup G) (s : Set G) (hs : s = ↑K), ↑(K.copy s hs) = s
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- State for all `CommRing` types detected by `grind`.  -/
Lean.Meta.Grind.Arith.CommRing.State : Type
-- Std.Time.Zoned.ZoneRules
_private.Std.Time.Zoned.ZoneRules.0.Std.Time.TimeZone.RecurringRule.transitionUtcSeconds : Std.Time.TimeZone.TransitionRule → Std.Time.Year.Offset → Std.Time.TimeZone.Offset → Std.Time.Second.Offset
-- Mathlib.RingTheory.RingHom.Flat
RingHom.Flat.ofLocalizationSpanTarget : RingHom.OfLocalizationSpanTarget fun {R S} [CommRing R] [CommRing S] => RingHom.Flat
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.evalFunCases : Lean.Elab.Tactic.Tactic
-- Mathlib.Data.Num.Lemmas
Num.castNum_shiftLeft : ∀ (m : Num) (n : ℕ), ↑(m <<< n) = ↑m <<< n
-- Mathlib.Topology.Order.UpperLowerSetTopology
OrderDual.instIsLowerSet : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsUpperSet α], Topology.IsLowerSet αᵒᵈ
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.maxEntry! : {α : Type u} → {β : α → Type v} → [Inhabited ((a : α) × β a)] → Std.DTreeMap.Internal.Impl α β → (a : α) × β a
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
IsSymmetricAlgebra.lift.eq_1 : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_3}
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] {f : M →ₗ[R] A} (h : IsSymmetricAlgebra f) {A' : Type u_4}
  [inst_5 : CommSemiring A'] [inst_6 : Algebra R A'] (g : M →ₗ[R] A'),
  h.lift g = (SymmetricAlgebra.lift g).comp ↑h.equiv.symm
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex
SSet.horn.IsCompatible.liftOfKanComplex.congr_simp : ∀ {X : SSet} {n : ℕ} {i : Fin (n + 2)} {f f_1 : (j : Fin (n + 2)) → j ≠ i → (SSet.stdSimplex.obj { len := n } ⟶ X)}
  (e_f : f = f_1) [inst : X.KanComplex] (hf : SSet.horn.IsCompatible f), hf.liftOfKanComplex = ⋯.liftOfKanComplex
-- Mathlib.FieldTheory.Relrank
IntermediateField.relrank_mul_relrank : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B C : IntermediateField F E},
  A ≤ B → B ≤ C → A.relrank B * B.relrank C = A.relrank C
-- Mathlib.Algebra.Homology.HomologicalComplex
/-- The obvious isomorphism `K.X p ≅ K.X q` when `p = q`.  -/
HomologicalComplex.XIsoOfEq : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
        {c : ComplexShape ι} → (K : HomologicalComplex V c) → {p q : ι} → p = q → (K.X p ≅ K.X q)
-- Mathlib.Analysis.Calculus.ContDiff.Operations
ContDiffOn.div_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {𝕜' : Type u_6} [inst_3 : NormedField 𝕜'] [inst_4 : NormedAlgebra 𝕜 𝕜']
  {f : E → 𝕜'} {n : WithTop ℕ∞}, ContDiffOn 𝕜 n f s → ∀ (c : 𝕜'), ContDiffOn 𝕜 n (fun x => f x / c) s
-- Mathlib.Algebra.Homology.ShortComplex.QuasiIso
CategoryTheory.ShortComplex.QuasiIso.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology] {φ : S₁ ⟶ S₂},
  CategoryTheory.IsIso (CategoryTheory.ShortComplex.homologyMap φ) → CategoryTheory.ShortComplex.QuasiIso φ
-- Init.Data.Array.Lemmas
Array.filterMap_some_fun : ∀ {α : Type u_1}, (fun as => Array.filterMap some as) = id
-- Batteries.Data.Fin.Lemmas
Fin.findSome?_eq_findSome?_finRange : ∀ {n : ℕ} {α : Type u_1} (f : Fin n → Option α), Fin.findSome? f = List.findSome? f (List.finRange n)
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.ιTruncLE_naturality_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : ∀ (i : ℤ), HomologicalComplex.HasHomology K i] [inst_4 : ∀ (i : ℤ), HomologicalComplex.HasHomology L i]
  (n : ℤ) {Z : CochainComplex C ℤ} (h : L ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CochainComplex.truncLEMap φ n)
      (CategoryTheory.CategoryStruct.comp (L.ιTruncLE n) h) =
    CategoryTheory.CategoryStruct.comp (K.ιTruncLE n) (CategoryTheory.CategoryStruct.comp φ h)
-- Mathlib.Topology.Category.LightProfinite.Extend
LightProfinite.Extend.functorOp_map : ∀ {F : CategoryTheory.Functor ℕᵒᵖ FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toLightProfinite))
  {X Y : ℕ} (f : X ⟶ Y),
  (LightProfinite.Extend.functorOp c).map f = CategoryTheory.CostructuredArrow.homMk (F.map f.op).op ⋯
-- Mathlib.Computability.Language
Language.mem_add : ∀ {α : Type u_1} (l m : Language α) (x : List α), x ∈ l + m ↔ x ∈ l ∨ x ∈ m
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.PolyDerivation.input.injEq : ∀ (p p_1 : Lean.Grind.CommRing.Poly),
  (Lean.Meta.Grind.Arith.CommRing.PolyDerivation.input p = Lean.Meta.Grind.Arith.CommRing.PolyDerivation.input p_1) =
    (p = p_1)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso_inv_comp_iCycles_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData) [inst_2 : S.HasLeftHomology] {Z : C} (h_1 : S.X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp h.cyclesIso.inv (CategoryTheory.CategoryStruct.comp S.iCycles h_1) =
    CategoryTheory.CategoryStruct.comp h.i h_1
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.pellZd_sub : ∀ {a : ℕ} (a1 : 1 < a) {m n : ℕ}, n ≤ m → Pell.pellZd a1 (m - n) = Pell.pellZd a1 m * star (Pell.pellZd a1 n)
-- Init.Data.List.Attach
List.pmap_attachWith : ∀ {α : Type u_1} {q : α → Prop} {β : Type u_2} {l : List α} {p : { x // q x } → Prop} {f : (a : { x // q x }) → p a → β}
  (H₁ : ∀ x ∈ l, q x) (H₂ : ∀ a ∈ l.attachWith q H₁, p a),
  List.pmap f (l.attachWith q H₁) H₂ = List.pmap (fun a h => f ⟨a, ⋯⟩ ⋯) l ⋯
-- Lean.Modifiers
Lean.protectedExt : Lean.TagDeclarationExtension
-- Mathlib.ModelTheory.Semantics
/-- Two structures are elementarily equivalent when they satisfy the same sentences.  -/
FirstOrder.Language.ElementarilyEquivalent : (L : FirstOrder.Language) → (M : Type w) → (N : Type u_1) → [L.Structure M] → [L.Structure N] → Prop
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.and_or_right : ∀ {σs : List (Type u)} {P Q R : Std.Do.SPred σs}, P ∧ Q ∨ R ⊣⊢ₛ (P ∨ R) ∧ (Q ∨ R)
-- Mathlib.MeasureTheory.Measure.Haar.Unique
/-- If an invariant measure is inner regular, then it gives the same mass to measurable sets with
compact closure as any other invariant measure, up to the scalar `addHaarScalarFactor μ' μ`.

Auxiliary lemma in the proof of the more general
`measure_isAddInvariant_eq_smul_of_isCompact_closure`, which works for any set with
compact closure, and removes the inner regularity assumption.  -/
MeasureTheory.Measure.measure_isAddInvariant_eq_smul_of_isCompact_closure_of_innerRegularCompactLTTop : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [LocallyCompactSpace G] (μ' μ : MeasureTheory.Measure G)
  [inst_6 : μ.IsAddHaarMeasure] [inst_7 : MeasureTheory.IsFiniteMeasureOnCompacts μ'] [inst_8 : μ'.IsAddLeftInvariant]
  [μ.InnerRegularCompactLTTop] {s : Set G},
  MeasurableSet s → IsCompact (closure s) → μ' s = μ'.addHaarScalarFactor μ • μ s
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsPos.cons_iff : ∀ {hd : ℝ} {tl : Tactic.ComputeAsymptotics.UnitMonomial},
  Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsPos (hd :: tl) ↔ 0 < hd ∨ hd = 0 ∧ tl.FirstNonzeroIsPos
-- Mathlib.CategoryTheory.Center.Basic
CategoryTheory.CatCenter.mul_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (x y : CategoryTheory.CatCenter C) (X : C),
  (x * y).app X = CategoryTheory.CategoryStruct.comp (x.app X) (y.app X)
-- Mathlib.RingTheory.Polynomial.Basic
Polynomial.mem_degreeLT : ∀ {R : Type u} [inst : Semiring R] {n : ℕ} {f : Polynomial R}, f ∈ Polynomial.degreeLT R n ↔ f.degree < ↑n
-- Init.Data.SInt.Bitwise
Int8.xor_neg_one : ∀ {a : Int8}, a ^^^ -1 = ~~~a
-- Init.Data.Slice.Array.Lemmas
Subarray.toArray_mkSlice_rio : ∀ {α : Type u_1} {xs : Subarray α} {hi : ℕ},
  Std.Slice.toArray (Std.Rio.Sliceable.mkSlice xs *...hi) = (Std.Slice.toArray xs).extract 0 hi
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
_private.Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing.0.AlgebraicGeometry.SheafedSpace.GlueData.«term𝖣» : Lean.ParserDescr
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.interSmallerFn : {α : Type u} →
  {β : α → Type v} →
    [BEq α] →
      [Hashable α] →
        Std.DHashMap.Internal.Raw₀ α β → Std.DHashMap.Internal.Raw₀ α β → α → Std.DHashMap.Internal.Raw₀ α β
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.unop_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex Cᵒᵖ), S.unop.f = S.g.unop
-- Mathlib.Topology.UniformSpace.Dini
/-- **Dini's theorem**: if `F n` is a monotone decreasing collection of continuous functions on a
converging pointwise to a continuous function `f`, then `F n` converges locally uniformly to `f`.  -/
Antitone.tendstoLocallyUniformly_of_forall_tendsto : ∀ {ι : Type u_1} {α : Type u_2} {G : Type u_3} [inst : Preorder ι] [inst_1 : TopologicalSpace α]
  [inst_2 : NormedAddCommGroup G] [inst_3 : Lattice G] [HasSolidNorm G] [IsOrderedAddMonoid G] {F : ι → α → G}
  {f : α → G},
  (∀ (i : ι), Continuous (F i)) →
    Antitone F →
      Continuous f →
        (∀ (x : α), Filter.Tendsto (fun x_1 => F x_1 x) Filter.atTop (nhds (f x))) →
          TendstoLocallyUniformly F f Filter.atTop
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.functoriality.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C)
  (G : CategoryTheory.Functor C D),
  CategoryTheory.Limits.Cocone.functoriality F G =
    { obj := fun A => { pt := G.obj A.pt, ι := CategoryTheory.NatTrans.mk' (fun j => G.map (A.ι.app j)) ⋯ },
      map := fun {Y X} f => { hom := G.map f.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Measurable.fst : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
  {f : α → β × γ}, Measurable f → Measurable fun a => (f a).1
-- Mathlib.Computability.Language
Language.reverse_add : ∀ {α : Type u_1} (l m : Language α), (l + m).reverse = l.reverse + m.reverse
-- Mathlib.Topology.Order.LeftRightLim
Antitone.rightLim_le : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
  [inst_2 : TopologicalSpace β] [OrderTopology β] {f : α → β},
  Antitone f → ∀ {x y : α}, x ≤ y → Function.rightLim f y ≤ f x
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
ApproximatesLinearOn.toOpenPartialHomeomorph_source : ∀ {𝕜 : 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} (s : Set E) {c : NNReal} [inst_5 : CompleteSpace E] (hf : ApproximatesLinearOn f (↑f') s c)
  (hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹) (hs : IsOpen s),
  (ApproximatesLinearOn.toOpenPartialHomeomorph f s hf hc hs).source = s
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.measure_smul_eq_zero_iff : ∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : Group G] [inst_1 : MulAction G α]
  {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] {s : Set α} (c : G), μ (c • s) = 0 ↔ μ s = 0
-- Mathlib.Algebra.CharP.Algebra
Subfield.charP : ∀ {R : Type u_1} [inst : DivisionRing R] (L : Subfield R) (p : ℕ) [CharP R p], CharP (↥L) p
-- Lean.Setup
Lean.instToJsonImport.toJson : Lean.Import → Lean.Json
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.orderIsoOfIso.eq_1 : ∀ {x y : SimplexCategory} (e : x ≅ y),
  SimplexCategory.orderIsoOfIso e =
    { toFun := ⇑(SimplexCategory.Hom.toOrderHom e.hom), invFun := ⇑(SimplexCategory.Hom.toOrderHom e.inv),
          left_inv := ⋯, right_inv := ⋯ }.toOrderIso
      ⋯ ⋯
-- Mathlib.Algebra.Homology.Embedding.Connect
CochainComplex.ConnectData.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} [inst_2 : SizeOf C] (d₀ : K.X 0 ⟶ L.X 0)
  (comp_d₀ : CategoryTheory.CategoryStruct.comp (K.d 1 0) d₀ = 0)
  (d₀_comp : CategoryTheory.CategoryStruct.comp d₀ (L.d 0 1) = 0),
  sizeOf { d₀ := d₀, comp_d₀ := comp_d₀, d₀_comp := d₀_comp } = 1 + sizeOf d₀ + sizeOf comp_d₀ + sizeOf d₀_comp
-- Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
ProbabilityTheory.IsGaussianProcess.hasGaussianLaw_fun_add : ∀ {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],
  ProbabilityTheory.IsGaussianProcess X P → ∀ {s t : T}, ProbabilityTheory.HasGaussianLaw (fun ω => X s ω + X t ω) P
-- Mathlib.SetTheory.Ordinal.Notation
/-- Multiplication of ordinal notations  -/
NONote.instMul : Mul NONote
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxc.Iterator.Monadic.isPlausibleIndirectOutput_iff : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LE α] [inst_2 : DecidableLE α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [Std.PRange.LawfulUpwardEnumerable α] {it : Std.IterM Id α} {out : α},
  it.IsPlausibleIndirectOutput out ↔
    ∃ n, (it.internalState.next.bind fun x => Std.PRange.succMany? n x) = some out ∧ out ≤ it.internalState.upperBound
-- Mathlib.Algebra.CharP.Defs
CharP.ringChar_ne_one : ∀ {R : Type u_1} [inst : NonAssocSemiring R] [Nontrivial R], ringChar R ≠ 1