mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.String.Lemmas.FindPos
String.posGE_eq_iff : ∀ {s : String} {p : String.Pos.Raw} {h : p ≤ s.rawEndPos} {q : s.Pos},
  s.posGE p h = q ↔ p ≤ q.offset ∧ ∀ (q' : s.Pos), p ≤ q'.offset → q ≤ q'
-- Lean.Meta.Tactic.Grind.Types
/-- Creates a congruence theorem for a `f`-applications with `numArgs` arguments.
 -/
Lean.Meta.Grind.mkHCongrWithArity : Lean.Expr → ℕ → Lean.Meta.Grind.GrindM Lean.Meta.CongrTheorem
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.pOpcycles.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) [inst_2 : K.HasHomology i],
  K.pOpcycles i = (K.sc i).pOpcycles
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.lt_slice_iff : ∀ {s : String.Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} {h₀ : p₀ ≤ q} {h₁ : q ≤ p₁},
  p < q.slice p₀ p₁ h₀ h₁ ↔ String.Slice.Pos.ofSlice p < q
-- Mathlib.RingTheory.Bialgebra.TensorProduct
Bialgebra.mulBialgHom_toAlgHom : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Bialgebra R A],
  ↑(Bialgebra.mulBialgHom R A) = Algebra.TensorProduct.lmul' R
-- Mathlib.Order.UpperLower.Closure
subset_upperClosure : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, s ⊆ ↑(upperClosure s)
-- Mathlib.CategoryTheory.Functor.FunctorHom
CategoryTheory.Functor.functorHomEquiv_apply_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (F G : CategoryTheory.Functor C D) (A : CategoryTheory.Functor C (Type (max u v v'))) (φ : A ⟶ F.functorHom G) (X : C)
  (a : A.obj X),
  ((F.functorHomEquiv G A) φ).app X a =
    ((CategoryTheory.ConcreteCategory.hom (φ.app X)) a).app X
      (CategoryTheory.CategoryStruct.id (Opposite.unop (Opposite.op X)))
-- Mathlib.CategoryTheory.PUnit
CategoryTheory.Functor.equiv_counitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.Functor.equiv.counitIso = CategoryTheory.NatIso.ofComponents CategoryTheory.Iso.refl ⋯
-- Lean.Data.Options
Lean.OptionDeprecation.mk : String → Option String → Lean.OptionDeprecation
-- Lean.Elab.App
/-- Process a `fType` of the form `{{x : A}} → B x`.
This method assume `fType` is a function type  -/
_private.Lean.Elab.App.0.Lean.Elab.Term.ElabAppArgs.processStrictImplicitArg : Lean.Name → Lean.Elab.Term.ElabAppArgs.M Lean.Expr
-- Lean.Meta.Tactic.Grind.MatchCond
/-- Given `e` a `match`-expression condition, returns the left-hand side
of the ground equations, and its type if it is the left-hand side of
a heterogeneous equality.
 -/
_private.Lean.Meta.Tactic.Grind.MatchCond.0.Lean.Meta.Grind.collectMatchCondLhss : Lean.Expr → Array (Lean.Expr × Option Lean.Expr)
-- Mathlib.Analysis.InnerProductSpace.Spectrum
/-- The eigenvalues for a self-adjoint operator `T` on a
finite-dimensional inner product space `E`, sorted in decreasing order  -/
LinearMap.IsSymmetric.eigenvalues : {𝕜 : Type u_3} →
  [inst : RCLike 𝕜] →
    {E : Type u_4} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : InnerProductSpace 𝕜 E] →
          {T : E →ₗ[𝕜] E} → [FiniteDimensional 𝕜 E] → {n : ℕ} → T.IsSymmetric → Module.finrank 𝕜 E = n → Fin n → ℝ
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.isClique_induce_iff : ∀ {α : Type u_1} {G : SimpleGraph α} {s : Set α} {t : Set ↑s},
  (SimpleGraph.induce s G).IsClique t ↔ G.IsClique (Subtype.val '' t)
-- Mathlib.Order.WellFounded
Set.range_injOn_strictMono : ∀ {β : Type u_2} {γ : Type u_3} [inst : LinearOrder β] [inst_1 : Preorder γ] [WellFoundedLT β],
  Set.InjOn Set.range {f | StrictMono f}
-- Mathlib.Tactic.Positivity.Basic
Mathlib.Meta.Positivity.ite_ne_zero_of_ne_zero_of_pos : ∀ {α : Type u_1} [inst : Zero α] (p : Prop) [inst_1 : Decidable p] {a b : α} [inst_2 : Preorder α],
  a ≠ 0 → 0 < b → (if p then a else b) ≠ 0
-- Mathlib.CategoryTheory.Bicategory.Opposites
Bicategory.Opposite.Hom2.op2'.injEq : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : Bᵒᵖ} {f g : a ⟶ b} (unop2 unop2_1 : f.unop ⟶ g.unop),
  ({ unop2 := unop2 } = { unop2 := unop2_1 }) = (unop2 = unop2_1)
-- Mathlib.Analysis.Calculus.ParametricIntervalIntegral
/-- Derivative under integral of `x ↦ ∫ F x a` at a given point `x₀ : 𝕜`, `𝕜 = ℝ` or `𝕜 = ℂ`,
assuming `F x₀` is integrable, `x ↦ F x a` is differentiable on a neighborhood of `x₀` for ae `a`
(with a neighborhood independent of `a`) with derivative uniformly bounded by an integrable
function, and `F x` is ae-measurable for `x` in a possibly smaller neighborhood of `x₀`.  -/
intervalIntegral.hasDerivAt_integral_of_dominated_loc_of_deriv_le : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {μ : MeasureTheory.Measure ℝ} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedSpace 𝕜 E] {a b : ℝ} {bound : ℝ → ℝ} {F F' : 𝕜 → ℝ → E} {x₀ : 𝕜}
  {s : Set 𝕜},
  s ∈ nhds x₀ →
    (∀ᶠ (x : 𝕜) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Set.uIoc a b))) →
      IntervalIntegrable (F x₀) μ a b →
        MeasureTheory.AEStronglyMeasurable (F' x₀) (μ.restrict (Set.uIoc a b)) →
          (∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → ∀ x ∈ s, ‖F' x t‖ ≤ bound t) →
            IntervalIntegrable bound μ a b →
              (∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → ∀ x ∈ s, HasDerivAt (fun x => F x t) (F' x t) x) →
                IntervalIntegrable (F' x₀) μ a b ∧
                  HasDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_const_mul_left : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (c : ℝ),
  ProbabilityTheory.covariance (fun ω => c * X ω) Y μ = c * ProbabilityTheory.covariance X Y μ
-- Mathlib.Data.Rel
/-- A relation `R` is symmetric if `a ~[R] b ↔ b ~[R] a`.  -/
SetRel.IsSymm : {α : Type u_1} → SetRel α α → Prop
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_maxKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {he : t ≠ ∅}, t.getKey? (t.maxKey he) = some (t.maxKey he)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.Struct.zsmulFn? : Lean.Meta.Grind.Arith.Linear.Struct → Option Lean.Expr
-- Mathlib.Order.Filter.Defs
/-- The principal filter of `s` is the collection of all supersets of `s`.  -/
Filter.term𝓟 : Lean.ParserDescr
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ResolvableCompletionItemData : Type
-- Mathlib.Order.LiminfLimsup
Filter.blimsup_or_eq_sup : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteDistribLattice α] {f : Filter β} {p q : β → Prop} {u : β → α},
  (Filter.blimsup u f fun x => p x ∨ q x) = Filter.blimsup u f p ⊔ Filter.blimsup u f q
-- Mathlib.Control.Fix
/-- `fix f` represents the computation of a fixed point for `f`.  -/
Fix.fix : {α : Type u_3} → [self : Fix α] → (α → α) → α
-- Aesop.Rule.Name
_private.Aesop.Rule.Name.0.Aesop.DisplayRuleName.toJsonRuleName : Aesop.DisplayRuleName → Aesop.RuleName
-- Mathlib.GroupTheory.Congruence.Defs
/-- Congruence relations equal the smallest congruence relation in which they are contained.  -/
Con.conGen_of_con : ∀ {M : Type u_1} [inst : Mul M] (c : Con M), conGen ⇑c = c
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.restrictScalarsId'_hom_app_hom_apply : ∀ {R : Type u_1} [inst : CommRing R] (f : R →+* R) (hf : f = RingHom.id R) (X : AlgCat R) (a : ↑X),
  (AlgCat.Hom.hom ((AlgCat.restrictScalarsId' f hf).hom.app X)) a = a
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.contains_iff_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} {k : α}, t.contains k = true ↔ k ∈ t
-- Mathlib.Order.Interval.Finset.Fin
Fin.Ioi_sub_one_eq_Ici : ∀ {n : ℕ} {a : Fin n}, 0 < a → Finset.Ioi (a - 1) = Finset.Ici a
-- Std.Time.Time.Unit.Minute
Std.Time.Minute.instLawfulEqOrdOrdinal : Std.LawfulEqOrd Std.Time.Minute.Ordinal
-- Mathlib.CategoryTheory.Widesubcategory
CategoryTheory.WideSubcategory.ext_iff : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {_P : CategoryTheory.MorphismProperty C}
  {inst_1 : _P.IsMultiplicative} {x y : CategoryTheory.WideSubcategory _P}, x = y ↔ x.obj = y.obj
-- Mathlib.RingTheory.DividedPowers.RatAlgebra
/-- There are no other divided power structures on an ideal of a  `ℚ`-algebra.  -/
DividedPowers.RatAlgebra.dividedPowers_unique : ∀ {R : Type u_1} [inst : CommSemiring R] {I : Ideal R} [inst_1 : DecidablePred fun x => x ∈ I] [inst_2 : Algebra ℚ R]
  (hI : DividedPowers I), hI = DividedPowers.RatAlgebra.dividedPowers I
-- Mathlib.Order.Defs.LinearOrder
compare_lt_iff_lt : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, compare a b = Ordering.lt ↔ a < b
-- Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
/-- For fixed `x : ℝ`, the mapping `mulExpNegMulSq ε x` converges pointwise to `x` as `ε → 0`  -/
Real.tendsto_mulExpNegMulSq : ∀ {x : ℝ}, Filter.Tendsto (fun ε => ε.mulExpNegMulSq x) (nhds 0) (nhds x)
-- Mathlib.AlgebraicTopology.SimplicialSet.PushoutProduct
SSet.Subcomplex.unionProd.ιIso_inv_left : ∀ {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex), (SSet.Subcomplex.unionProd.ιIso S T).inv.left = ⋯.isoPushout.inv
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey!_eq_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [inst : Inhabited α], t.WF → ∀ {k : α}, k ∈ t → t.getKey! k = k
-- Mathlib.Order.GaloisConnection.Defs
GaloisConnection.l_u_le : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {u : α → β} {l : β → α},
  GaloisConnection l u → ∀ (a : α), l (u a) ≤ a
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
AddSubgroup.op_iInf : ∀ {ι : Sort u_1} {G : Type u_2} [inst : AddGroup G] (S : ι → AddSubgroup G), (iInf S).op = ⨅ i, (S i).op
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Measurable.sSup : ∀ {α : Type u_1} {δ : Type u_4} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α]
  {mδ : MeasurableSpace δ} [inst_2 : ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α]
  {ι : Type u_5} {f : ι → δ → α} {s : Set ι},
  s.Countable → (∀ i ∈ s, Measurable (f i)) → Measurable fun x => sSup ((fun i => f i x) '' s)
-- Mathlib.Tactic.FunProp.Decl
/-- Returns function property declaration from `e = P f`.  -/
Mathlib.Meta.FunProp.getFunPropDecl? : Lean.Expr → Lean.MetaM (Option Mathlib.Meta.FunProp.FunPropDecl)
-- Mathlib.Algebra.Ring.Pi
NonUnitalRingHom.pi_injective : ∀ {I : Type u} {f : I → Type u_1} {γ : Type u_2} [Nonempty I] [inst : (i : I) → NonUnitalNonAssocSemiring (f i)]
  [inst_1 : NonUnitalNonAssocSemiring γ] (g : (i : I) → γ →ₙ+* f i),
  (∀ (i : I), Function.Injective ⇑(g i)) → Function.Injective ⇑(NonUnitalRingHom.pi g)
-- Std.Http.Server.Connection
Std.Http.Server.Connection.mk : {α : Type} →
  α →
    Std.Http.Protocol.H1.Machine Std.Http.Protocol.H1.Direction.receiving →
      Std.Http.Extensions → Std.Http.Server.Connection α
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.tryTactic? : {α : Type} → Lean.Elab.Tactic.Grind.GrindTacticM α → Lean.Elab.Tactic.Grind.GrindTacticM (Option α)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PullbackObjObj.π_snd_assoc : ∀ {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₃]
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₃ Y₃ : C₃}
  {f₃ : X₃ ⟶ Y₃} (self : G.PullbackObjObj f₁ f₃) {Z : C₂} (h : (G.obj (Opposite.op Y₁)).obj Y₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.π (CategoryTheory.CategoryStruct.comp self.snd h) =
    CategoryTheory.CategoryStruct.comp ((G.obj (Opposite.op Y₁)).map f₃) h
-- Lean.Data.PrefixTree
Lean.PrefixTree.empty : {α : Type u_1} → {β : Type u_2} → {p : α → α → Ordering} → Lean.PrefixTree α β p
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.getD_union : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k fallback : α},
  (t₁ ∪ t₂).getD k fallback = t₂.getD k (t₁.getD k fallback)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.map_id_fun : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], Std.ExtHashMap.map (fun x v => v) m = m
-- Mathlib.Data.Finset.SymmDiff
Finset.symmDiff_eq_empty : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, symmDiff s t = ∅ ↔ s = t
-- Init.Internal.Order.Basic
Lean.Order.flat_csup_eq : ∀ {α : Sort u} {b : α} (c : Lean.Order.FlatOrder b → Prop) (hchain : Lean.Order.chain c),
  Lean.Order.flat_csup c = Lean.Order.CCPO.csup hchain
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem_insert_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β}, (m.insert k v)[k] = v
-- Aesop.RuleSet
Aesop.LocalRuleSet.applicableNormalizationRules : Aesop.LocalRuleSet →
  Aesop.ForwardRuleMatches → Lean.MVarId → Aesop.BaseM (Array (Aesop.IndexMatchResult Aesop.NormRule))
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.leftKanExtensionUnique.congr_simp : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α α_1 : F ⟶ L.comp F') (e_α : α = α_1) [inst_3 : F'.IsLeftKanExtension α] (F'' : CategoryTheory.Functor D H)
  (α' α'_1 : F ⟶ L.comp F'') (e_α' : α' = α'_1) [inst_4 : F''.IsLeftKanExtension α'],
  F'.leftKanExtensionUnique α F'' α' = F'.leftKanExtensionUnique α_1 F'' α'_1
-- Mathlib.Algebra.BrauerGroup.Defs
/-- Any member of `CSA` is simple.  -/
CSA.isSimple : ∀ {K : Type u} [inst : Field K] (self : CSA K), IsSimpleRing ↑self.toAlgCat
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get_eq_getD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a fallback : α} {h' : a ∈ t}, t.get a h' = t.getD a fallback
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- `K.opcycles j` is the cokernel of `K.d i j` when `c.prev j = i`.  -/
HomologicalComplex.opcyclesIsCokernel : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          (K : HomologicalComplex C c) →
            (i j : ι) →
              [K.HasHomology i] →
                c.prev j = i →
                  [inst_3 : K.HasHomology j] →
                    CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ (K.pOpcycles j) ⋯)
-- Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
CochainComplex.triangleOfDegreewiseSplit_obj₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (S : CategoryTheory.ShortComplex (CochainComplex C ℤ))
  (σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting),
  (CochainComplex.triangleOfDegreewiseSplit S σ).obj₂ = S.X₂
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
SSet.Subcomplex.PairingCore.RankFunction.mk.inj : ∀ {X : SSet} {A : X.Subcomplex} {h : A.PairingCore} {α : Type v} {inst : PartialOrder α} {rank : h.ι → α}
  {lt : ∀ {x y : h.ι}, h.AncestralRel x y → rank x < rank y} {rank_1 : h.ι → α}
  {lt_1 : ∀ {x y : h.ι}, h.AncestralRel x y → rank_1 x < rank_1 y},
  { rank := rank, lt := lt } = { rank := rank_1, lt := lt_1 } → rank = rank_1
-- Init.Data.UInt.Bitwise
UInt32.ofFin_xor : ∀ (a b : Fin UInt32.size), UInt32.ofFin (a ^^^ b) = UInt32.ofFin a ^^^ UInt32.ofFin b
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionIdentifier.const.sizeOf_spec : ∀ (declName : Lean.Name), sizeOf (Lean.Lsp.CompletionIdentifier.const declName) = 1 + sizeOf declName
-- Mathlib.CategoryTheory.Filtered.Final
/-- Any over category on a cofiltered or empty category is cofiltered.
(Note that over categories are always filtered since they have a terminal object.)  -/
CategoryTheory.IsCofiltered.over : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.IsCofilteredOrEmpty C] (c : C),
  CategoryTheory.IsCofiltered (CategoryTheory.Over c)
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Expr : Type
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.instQuasiIsoAtOppositeMapSymmOpFunctorOp : ∀ {ι : Type u_1} {V : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} V] {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {K L : HomologicalComplex V c} (φ : K ⟶ L) (i : ι)
  [inst_2 : K.HasHomology i] [inst_3 : L.HasHomology i] [QuasiIsoAt φ i],
  QuasiIsoAt ((HomologicalComplex.opFunctor V c).map φ.op) i
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_of_restrict_of_restrict_compl : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β} {s : Set α},
  MeasurableSet s → Measurable (s.domRestrict f) → Measurable (sᶜ.domRestrict f) → Measurable f
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
SSet.horn₃₁.desc.congr_simp : ∀ {X : SSet} (f₀ f₀_1 : SSet.stdSimplex.obj { len := 2 } ⟶ X) (e_f₀ : f₀ = f₀_1)
  (f₂ f₂_1 : SSet.stdSimplex.obj { len := 2 } ⟶ X) (e_f₂ : f₂ = f₂_1) (f₃ f₃_1 : SSet.stdSimplex.obj { len := 2 } ⟶ X)
  (e_f₃ : f₃ = f₃_1)
  (h₁₂ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₃)
  (h₁₃ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 1) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₂)
  (h₂₃ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₂ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₃),
  SSet.horn₃₁.desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃ = SSet.horn₃₁.desc f₀_1 f₂_1 f₃_1 ⋯ ⋯ ⋯
-- Mathlib.CategoryTheory.ConcreteCategory.Bundled
/-- The corresponding instance of the bundled type class  -/
CategoryTheory.Bundled.str : {c : Type u → Type v} → (self : CategoryTheory.Bundled c) → c ↑self
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.GeneralLinearGroup.coe_scalar : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : Semiring R] (u : Rˣ),
  ↑((Matrix.GeneralLinearGroup.scalar n) u) = (Matrix.scalar n) ↑u
-- Mathlib.LinearAlgebra.QuadraticForm.Signature
/-- Defining property of `sigPos`.  -/
sigPos_isGreatest : ∀ {R : Type u_1} {M : Type u_2} [inst : AddCommGroup M] [inst_1 : CommRing R] [inst_2 : LinearOrder R]
  [inst_3 : Module R M] (Q : QuadraticForm R M) [Module.Finite R M] [StrongRankCondition R],
  IsGreatest {r | ∃ V, Module.finrank R ↥V = r ∧ (QuadraticMap.restrict Q V).PosDef} (sigPos Q)
-- Mathlib.Order.Hom.Basic
map_inv_le_map_inv_iff : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] [inst_2 : EquivLike F α β]
  [OrderIsoClass F α β] (f : F) {a b : β}, EquivLike.inv f b ≤ EquivLike.inv f a ↔ b ≤ a
-- Mathlib.MeasureTheory.Constructions.BorelSpace.WithTop
Measurable.withTop_coe : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι]
  [inst_3 : MeasurableSpace ι] [BorelSpace ι] {α : Type u_2} {mα : MeasurableSpace α} {f : α → ι},
  Measurable f → Measurable fun x => ↑(f x)
-- Mathlib.Data.Finset.Basic
/-- Given a finset `l` and a predicate `p`, associate to a proof that there is a unique element of
`l` satisfying `p` this unique element, as an element of the ambient type.  -/
Finset.choose : {α : Type u_1} → (p : α → Prop) → [DecidablePred p] → (l : Finset α) → (∃! a, a ∈ l ∧ p a) → α
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.pushMissing : Lean.Parser.ParserFn
-- Mathlib.LinearAlgebra.BilinearForm.Hom
/-- The linear map obtained from a `BilinForm` by fixing the right co-ordinate and evaluating in
the left.  -/
LinearMap.BilinForm.toLinHomFlip : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → LinearMap.BilinForm R M →ₗ[R] M →ₗ[R] M →ₗ[R] R
-- Init.Data.SInt.Bitwise
Int16.xor_right_inj : ∀ {a b : Int16} (c : Int16), c ^^^ a = c ^^^ b ↔ a = b
-- Mathlib.Tactic.BDSimp
/-- `bdsimp` definitionally simplifies the goal. This is a backward compatibility macro for `dsimp`.
Like `dsimp`, it applies only theorems that hold by reflexivity, and the result is guaranteed to be
definitionally equal to the input. The difference is that `bdsimp` allows any theorem whose proof is
reflexivity, while `dsimp` requires the proof to hold at `.instances` transparency level.

This tactic is a temporary workaround.
`bdsimp` also rewrites in depended-on positions, which means the result can fail to typecheck at
the expected `.instances` transparency level. For example:
```lean
@[expose] def two := 2
@[defeq] lemma two_eq : two = 2 := by rfl
instance : NeZero two := inferInstanceAs (NeZero 2)

example (x : Fin two) : x * 0 = 0 := by
  bdsimp only [two_eq]
  fail_if_success rw [Fin.mul_zero] -- Fails: `x : Fin two` but `· * · : Fin 2 → Fin 2 → Fin 2`
```

This tactic supports all options supported by `dsimp`.
 -/
bdsimp : Lean.ParserDescr
-- Mathlib.LinearAlgebra.Projection
LinearMap.IsProj.mk : ∀ {S : Type u_5} [inst : Semiring S] {M : Type u_6} [inst_1 : AddCommMonoid M] [inst_2 : Module S M] {m : Submodule S M}
  {F : Type u_7} [inst_3 : FunLike F M M] {f : F}, (∀ (x : M), f x ∈ m) → (∀ x ∈ m, f x = x) → LinearMap.IsProj m f
-- Mathlib.Order.CompleteLattice.Basic
iSup_mono' : ∀ {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [inst : CompleteLattice α] {f : ι → α} {g : ι' → α},
  (∀ (i : ι), ∃ i', f i ≤ g i') → iSup f ≤ iSup g
-- Mathlib.Data.Set.Finite.Lattice
iSup_iInf_of_antitone : ∀ {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [Finite ι] [inst : Preorder ι'] [Nonempty ι'] [IsCodirectedOrder ι']
  [inst_3 : Order.Frame α] {f : ι → ι' → α}, (∀ (i : ι), Antitone (f i)) → ⨆ j, ⨅ i, f i j = ⨅ i, ⨆ j, f i j
-- Lean.Parser.Command
Lean.Parser.Command.assertNotExists.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.MeasureTheory.Measure.Hausdorff
/-- If `c ∉ {0, ∞}` and `m₁ d ≤ c * m₂ d` for `d < ε` for some `ε > 0`
(we use `≤ᶠ[𝓝[≥] 0]` to state this), then `mkMetric m₁ hm₁ ≤ c • mkMetric m₂ hm₂`.  -/
MeasureTheory.OuterMeasure.mkMetric_mono_smul : ∀ {X : Type u_2} [inst : EMetricSpace X] {m₁ m₂ : ENNReal → ENNReal} {c : ENNReal},
  c ≠ ⊤ →
    c ≠ 0 →
      m₁ ≤ᶠ[nhdsWithin 0 (Set.Ici 0)] c • m₂ →
        MeasureTheory.OuterMeasure.mkMetric m₁ ≤ c • MeasureTheory.OuterMeasure.mkMetric m₂
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.spanningHom_apply : ∀ {V : Type u} {G : SimpleGraph V} (x : G.Subgraph) (a : V), x.spanningHom a = id a
-- Mathlib.RingTheory.SimpleRing.Field
isSimpleRing_iff_isField : ∀ (A : Type u_1) [inst : CommRing A], IsSimpleRing A ↔ IsField A
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.A_isSymm : ∀ (n : ℕ), (CartanMatrix.A n).IsSymm
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.singleton_disjoint_neighborFinset : ∀ {V : Type u_1} (G : SimpleGraph V) (v : V) [inst : Fintype ↑(G.neighborSet v)], Disjoint {v} (G.neighborFinset v)
-- Std.Http.Data.Headers.Value
Std.Http.Header.instDecidableEqValue.decEq : (x x_1 : Std.Http.Header.Value) → Decidable (x = x_1)
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.instHasOfPrecompPropertyIsomorphismsOfRespectsIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) [W.RespectsIso],
  W.HasOfPrecompProperty (CategoryTheory.MorphismProperty.isomorphisms C)
-- Mathlib.Data.List.DropRight
List.rtakeWhile.eq_1 : ∀ {α : Type u_1} (p : α → Bool) (l : List α), List.rtakeWhile p l = (List.takeWhile p l.reverse).reverse
-- Mathlib.Logic.Equiv.Basic
Equiv.ofFiberEquiv_apply : ∀ {α : Type u_13} {β : Type u_14} {γ : Type u_15} {f : α → γ} {g : β → γ}
  (e : (c : γ) → { a // f a = c } ≃ { b // g b = c }) (a : α),
  (Equiv.ofFiberEquiv e) a = ↑((e (f a)) ((Equiv.sigmaFiberEquiv f).symm a).snd)