mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
AEMeasurable.max : ∀ {α : Type u_1} {δ : Type u_4} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α]
  {mδ : MeasurableSpace δ} [inst_2 : LinearOrder α] [SecondCountableTopology α] [OrderClosedTopology α] {f g : δ → α}
  {μ : MeasureTheory.Measure δ}, AEMeasurable f μ → AEMeasurable g μ → AEMeasurable (fun a => max (f a) (g a)) μ
-- Mathlib.Topology.Continuous
DenseRange.mem_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x : X} {α : Type u_4} {f : α → X} {s : Set X},
  DenseRange f → s ∈ nhds x → ∃ a, f a ∈ s
-- Mathlib.Analysis.Analytic.RadiusLiminf
/-- The **Cauchy-Hadamard theorem** for formal multilinear series: The inverse of the radius
is equal to $\limsup_{n\to\infty} \sqrt[n]{‖p n‖}$.  -/
FormalMultilinearSeries.radius_inv_eq_limsup : ∀ {𝕜 : 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]
  (p : FormalMultilinearSeries 𝕜 E F), p.radius⁻¹ = Filter.limsup (fun n => ↑(‖p n‖₊ ^ (1 / ↑n))) Filter.atTop
-- Mathlib.CategoryTheory.Galois.IsFundamentalgroup
CategoryTheory.PreGaloisCategory.toAut_surjective_isGalois : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) (G : Type u_1)
  [inst_1 : Group G] [inst_2 : (X : C) → MulAction G (F.obj X).obj] [CategoryTheory.PreGaloisCategory.IsNaturalSMul F G]
  [inst_4 : CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F]
  (t : CategoryTheory.Aut F) (X : C) [CategoryTheory.PreGaloisCategory.IsGalois X]
  [MulAction.IsPretransitive G (F.obj X).obj],
  ∃ g, ∀ (x : (F.obj X).obj), g • x = (CategoryTheory.ConcreteCategory.hom (t.hom.app X)) x
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
String.Slice.Pattern.BackwardSliceSearcher.skipSuffix?.fun_cases_unfolding : ∀ (pat s : String.Slice) (motive : Option s.Pos → Prop),
  (String.Slice.Pattern.BackwardSliceSearcher.endsWith pat s = true →
      motive (some (s.pos! (s.endPos.offset.unoffsetBy pat.rawEndPos)))) →
    (¬String.Slice.Pattern.BackwardSliceSearcher.endsWith pat s = true → motive none) →
      motive (String.Slice.Pattern.BackwardSliceSearcher.skipSuffix? pat s)
-- Mathlib.CategoryTheory.FiberedCategory.Cartesian
CategoryTheory.Functor.IsStronglyCartesian.map_self : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [inst_2 : p.IsStronglyCartesian f φ],
  CategoryTheory.Functor.IsStronglyCartesian.map p f φ ⋯ φ = CategoryTheory.CategoryStruct.id a
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.var.sizeOf_spec : ∀ {L : FirstOrder.Language} {α : Type u'} [inst : SizeOf α] (a : α), sizeOf (FirstOrder.Language.var a) = 1 + sizeOf a
-- Mathlib.Logic.Equiv.Defs
Equiv.forall_congr_left : ∀ {α : Sort u} {β : Sort v} {p : α → Prop} (e : α ≃ β), (∀ (a : α), p a) ↔ ∀ (b : β), p (e.symm b)
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.Iter.forIn_filterWithPostcondition : ∀ {α β γ : Type w} [inst : Std.Iterator α Id β] {ps : Std.Do.PostShape} {n : Type w → Type u_1} {o : Type w → Type u_2}
  [inst_1 : Monad n] [LawfulMonad n] [inst_3 : Monad o] [LawfulMonad o] [inst_5 : Std.Do.WPMonad o ps]
  [inst_6 : MonadLiftT n o] [LawfulMonadLiftT n o] [Std.Iterators.Finite α Id] [inst_9 : Std.IteratorLoop α Id o]
  [Std.LawfulIteratorLoop α Id o] {it : Std.Iter β} {f : β → Std.Iterators.PostconditionT n (ULift.{w, 0} Bool)}
  {init : γ} {g : β → γ → o (ForInStep γ)} {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond γ ps},
  ⦃P⦄
      forIn it init fun out acc => do
        let __do_lift ← liftM (f out).run
        if __do_lift.down = true then g out acc else pure (ForInStep.yield acc) ⦃Q⦄ →
    ⦃P⦄ forIn (Std.Iter.filterWithPostcondition f it) init g ⦃Q⦄
-- Init.Data.UInt.Lemmas
UInt64.neg_add_mul_eq_mul_not : ∀ {a b : UInt64}, -(a + a * b) = a * ~~~b
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- `single a b` is the finitely supported function with value `b` at `a` and zero otherwise.  -/
SkewMonoidAlgebra.single : {k : Type u_1} → {G : Type u_2} → [inst : AddMonoid k] → G → k → SkewMonoidAlgebra k G
-- Mathlib.Order.Closure
LowerAdjoint.closure_iSup_closure : ∀ {α : Type u_1} {ι : Sort u_2} {β : Type u_4} [inst : CompleteLattice α] [inst_1 : Preorder β] {u : β → α}
  (l : LowerAdjoint u) (f : ι → α), u (l.toFun (⨆ i, u (l.toFun (f i)))) = u (l.toFun (⨆ i, f i))
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.map_map_equiv : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {γ : α → Type w}
  {δ : α → Type w'} {f : (a : α) → β a → γ a} {g : (a : α) → γ a → δ a},
  m.WF → (Std.DHashMap.Raw.map g (Std.DHashMap.Raw.map f m)).Equiv (Std.DHashMap.Raw.map (fun k v => g k (f k v)) m)
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
/-- **Alias** of `WithSeminorms.continuous_of_continuous_comp`. -/
Seminorm.continuous_of_continuous_comp : ∀ {𝕝 : Type u_4} {𝕝₂ : Type u_5} {E : Type u_6} {F : Type u_7} {ι' : Type u_10} [inst : AddCommGroup E]
  [inst_1 : NormedField 𝕝] [inst_2 : Module 𝕝 E] [inst_3 : AddCommGroup F] [inst_4 : NormedField 𝕝₂]
  [inst_5 : Module 𝕝₂ F] {τ₁₂ : 𝕝 →+* 𝕝₂} [inst_6 : RingHomIsometric τ₁₂] {q : SeminormFamily 𝕝₂ F ι'}
  [inst_7 : TopologicalSpace E] [IsTopologicalAddGroup E] [inst_9 : TopologicalSpace F],
  WithSeminorms q → ∀ (f : E →ₛₗ[τ₁₂] F), (∀ (i : ι'), Continuous ⇑((q i).comp f)) → Continuous ⇑f
-- Aesop.Search.Expansion.Norm
Aesop.NormM.State.forwardState : Aesop.NormM.State → Aesop.ForwardState
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
LinearIndependent.linearCombinationEquiv_apply_coe : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (hv : LinearIndependent R v) (x : ι →₀ R),
  ↑(hv.linearCombinationEquiv x) = (Finsupp.linearCombination R v) x
-- Mathlib.Computability.StateTransition
StateTransition.fun_respects : ∀ {σ₁ : Type u_1} {σ₂ : Type u_2} {f₁ : σ₁ → Option σ₁} {f₂ : σ₂ → Option σ₂} {tr : σ₁ → σ₂},
  (StateTransition.Respects f₁ f₂ fun a b => tr a = b) ↔ ∀ ⦃a₁ : σ₁⦄, StateTransition.FRespects f₂ tr (tr a₁) (f₁ a₁)
-- Mathlib.Order.Filter.AtTopBot.Monoid
Filter.Tendsto.atBot_mul_le_one : ∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] [inst_1 : Preorder M] [IsOrderedMonoid M] {l : Filter α}
  {f g : α → M},
  Filter.Tendsto f l Filter.atBot → (∀ (x : α), g x ≤ 1) → Filter.Tendsto (fun x => f x * g x) l Filter.atBot
-- Aesop.BuiltinRules.Subst
Aesop.BuiltinRules.prepareIff? : Lean.MVarId → Lean.FVarId → Aesop.ScriptM (Option (Lean.MVarId × Lean.FVarId))
-- Mathlib.Data.ZMod.Basic
ZMod.intCast_cast : ∀ {n : ℕ} {R : Type u_1} [inst : Ring R] (i : ZMod n), ↑i.cast = i.cast
-- Mathlib.Analysis.Complex.ExponentialBounds
Real.log_two_near_10 : |Real.log 2 - 287209 / 414355| ≤ 1 / 10 ^ 10
-- Mathlib.Tactic.Order.CollectFacts
Mathlib.Tactic.Order.AtomicFact.lt.inj : ∀ {lhs rhs : ℕ} {proof : Lean.Expr} {lhs_1 rhs_1 : ℕ} {proof_1 : Lean.Expr},
  Mathlib.Tactic.Order.AtomicFact.lt lhs rhs proof = Mathlib.Tactic.Order.AtomicFact.lt lhs_1 rhs_1 proof_1 →
    lhs = lhs_1 ∧ rhs = rhs_1 ∧ proof = proof_1
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.congrRightFunctor_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (e : C ≌ D),
  (CategoryTheory.Equivalence.congrRightFunctor E).obj e = e.congrRight
-- Mathlib.Geometry.Manifold.Instances.Sphere
stereographic'_target : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {n : ℕ}
  [inst_2 : Fact (Module.finrank ℝ E = n + 1)] (v : ↑(Metric.sphere 0 1)), (stereographic' n v).target = Set.univ
-- Lean.Elab.Tactic.Try
/-- If the current `try?` context is terminal, throws unless all goals have been solved.

`try?` handlers whose execution may leave goals open (e.g. `simp?`, generic atomic leaves) should
call this before returning their suggestion. Combinator handlers that delegate via `evalSuggest`
do not need to call it, since the recursive call already enforces the invariant on the
sub-tactic in terminal mode.
 -/
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.checkTerminalGoals : Lean.Elab.Tactic.Try.TryTacticM Unit
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
/-- **Fundamental theorem of calculus-2**, on semi-infinite intervals `(a, +∞)`.
When a function has a limit at infinity `m`, and its derivative is integrable, then the
integral of the derivative on `(a, +∞)` is `m - f a`. Version assuming differentiability
on `[a, +∞)`.

Note that such a function always has a limit at infinity,
see `tendsto_limUnder_of_hasDerivAt_of_integrableOn_Ioi`.  -/
MeasureTheory.integral_Ioi_of_hasDerivAt_of_tendsto' : ∀ {E : Type u_1} {f f' : ℝ → E} {a : ℝ} {m : E} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [CompleteSpace E],
  (∀ x ∈ Set.Ici a, HasDerivAt f (f' x) x) →
    MeasureTheory.IntegrableOn f' (Set.Ioi a) MeasureTheory.volume →
      Filter.Tendsto f Filter.atTop (nhds m) → ∫ (x : ℝ) in Set.Ioi a, f' x = m - f a
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
spectralAlgNorm_def : ∀ {K : Type u_2} [inst : NormedField K] {L : Type u_3} [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : IsUltrametricDist K] [h_alg : Algebra.IsAlgebraic K L] (x : L), (spectralAlgNorm K L) x = spectralNorm K L x
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
Polynomial.resultant_zero_left : ∀ {R : Type u_1} [inst : CommRing R] (g : Polynomial R) (m n : ℕ), Polynomial.resultant 0 g m n = 0 ^ n * g.coeff 0 ^ m
-- Mathlib.Data.Set.Subsingleton
/-- Extract witnesses from s.nontrivial. This function might be used instead of case analysis on the
argument. Note that it makes a proof depend on the classical.choice axiom.  -/
Set.Nontrivial.choose : {α : Type u} → {s : Set α} → s.Nontrivial → α × α
-- Mathlib.Analysis.Convex.Extreme
isExtreme_iInter : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {A : Set E} {ι : Sort u_6} [Nonempty ι] {F : ι → Set E},
  (∀ (i : ι), IsExtreme 𝕜 A (F i)) → IsExtreme 𝕜 A (⋂ i, F i)
-- Init.Data.Nat.Gcd
Nat.gcd_dvd : ∀ (m n : ℕ), m.gcd n ∣ m ∧ m.gcd n ∣ n
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry?_cons : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k},
  Std.Internal.List.getEntry? a (⟨k, v⟩ :: l) = bif k == a then some ⟨k, v⟩ else Std.Internal.List.getEntry? a l
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instCommSemigroup : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [CommSemigroup Y] → CommSemigroup (LocallyConstant X Y)
-- Mathlib.Data.Stream.Defs
/-- Append a stream to a list.  -/
Stream'.«term_++ₛ_» : Lean.TrailingParserDescr
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Subfield.extendScalars_top : ∀ {L : Type u_2} [inst : Field L] (F : Subfield L), Subfield.extendScalars ⋯ = ⊤
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.containsThenInsert_snd : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α}, (m.containsThenInsert k).2 = m.insert k
-- Mathlib.CategoryTheory.Generator.Basic
/-- We say that `P : ObjectProperty C` is detecting if the functors `C(G, -)`
for `G : C` such that `P G` collectively reflect isomorphisms,
i.e., if any `h` with domain `G` that `P G` uniquely factors through `f`,
then `f` is an isomorphism.  -/
CategoryTheory.ObjectProperty.IsDetecting : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.ObjectProperty C → Prop
-- Lean.Hygiene
Lean.Unhygienic.instMonadQuotation : Lean.MonadQuotation Lean.Unhygienic
-- Mathlib.Order.Heyting.Basic
sdiff_ne_sdiff_iff : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a \ b ≠ b \ a ↔ a ≠ b
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
/-- Given any pair of coprime elements of `R`, there exists a matrix in `SL(2, R)` having those
entries as its top or bottom row.  -/
IsCoprime.exists_SL2_row : ∀ {R : Type u_1} [inst : CommRing R] {a b : R}, IsCoprime a b → ∀ (i : Fin 2), ∃ g, ↑g i 0 = a ∧ ↑g i 1 = b
-- Mathlib.Control.Basic
guard_false : ∀ {F : Type → Type v} [inst : Alternative F] {h : Decidable False}, guard False = failure
-- Mathlib.Topology.CWComplex.Classical.Finite
/-- If the collection of all cells (of any dimension) of a relative CW complex `C` is finite, then
`C` is finite as a CW complex.  -/
Topology.RelCWComplex.finite_of_finite_cells : ∀ {X : Type u_2} [inst : TopologicalSpace X] {C D : Set X} [inst_1 : Topology.RelCWComplex C D],
  Finite ((n : ℕ) × Topology.RelCWComplex.cell C n) → Topology.RelCWComplex.Finite C
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
TensorProduct.finsuppScalarLeft_apply_tmul : ∀ {R : Type u_1} [inst : CommSemiring R] {N : Type u_4} [inst_1 : AddCommMonoid N] [inst_2 : Module R N] {ι : Type u_5}
  [inst_3 : DecidableEq ι] (p : ι →₀ R) (n : N),
  (TensorProduct.finsuppScalarLeft R N ι) (p ⊗ₜ[R] n) = p.sum fun i m => fun₀ | i => m • n
-- Mathlib.RepresentationTheory.FiniteIndex
Rep.indCoindIso.congr_simp : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Group G] {S : Subgroup G}
  [inst_2 : DecidableRel ⇑(QuotientGroup.rightRel S)] [inst_3 : S.FiniteIndex] (A : Rep.{max w u, u, v} k ↥S),
  A.indCoindIso = A.indCoindIso
-- Init.Data.UInt.Lemmas
UInt64.add_def : ∀ (a b : UInt64), a + b = { toBitVec := a.toBitVec + b.toBitVec }
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
ProbabilityTheory.Kernel.integral_integral_add_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : NormedAddCommGroup E] {a : α} {κ : ProbabilityTheory.Kernel α β}
  {η : ProbabilityTheory.Kernel β γ} [inst_1 : NormedSpace ℝ E] ⦃f g : γ → E⦄,
  MeasureTheory.Integrable f ((η.comp κ) a) →
    MeasureTheory.Integrable g ((η.comp κ) a) →
      ∫ (x : β), ∫ (y : γ), f y + g y ∂η x ∂κ a =
        ∫ (x : β), ∫ (y : γ), f y ∂η x ∂κ a + ∫ (x : β), ∫ (y : γ), g y ∂η x ∂κ a
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instSub : {α : Type u_1} → [Sub α] → Sub (Lex α)
-- Mathlib.ModelTheory.Algebra.Ring.Basic
FirstOrder.ringFunc.one : FirstOrder.ringFunc 0
-- Mathlib.Data.Multiset.Fintype
Multiset.coe_mk : ∀ {α : Type u_1} [inst : DecidableEq α] {m : Multiset α} {x : α} {i : Fin (Multiset.count x m)},
  (m.mkToType x i).fst = x
-- Mathlib.Topology.Algebra.Valued.WithVal
/-- **Alias** of `WithVal.valued_toVal`. -/
WithVal.apply_symm_equiv : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀)
  (r : R), Valued.v (WithVal.toVal v r) = v r
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.Waiter.consumerNode.injEq : ∀ (a a_1 : Lean.Meta.SynthInstance.ConsumerNode),
  (Lean.Meta.SynthInstance.Waiter.consumerNode a = Lean.Meta.SynthInstance.Waiter.consumerNode a_1) = (a = a_1)
-- Mathlib.CategoryTheory.Sites.LocallyBijective
CategoryTheory.Presheaf.isLocallySurjective_presheafToSheaf_map_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w'}
  [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [inst_3 : CategoryTheory.ConcreteCategory A FA]
  [inst_4 : CategoryTheory.HasWeakSheafify J A] [J.WEqualsLocallyBijective A] {P Q : CategoryTheory.Functor Cᵒᵖ A}
  (φ : P ⟶ Q),
  CategoryTheory.Sheaf.IsLocallySurjective ((CategoryTheory.presheafToSheaf J A).map φ) ↔
    CategoryTheory.Presheaf.IsLocallySurjective J φ
-- Mathlib.Data.Part
Part.ofOption.eq_1 : ∀ {α : Type u_1}, ↑none = Part.none
-- Lean.CoreM
Lean.Core.Context.ref : Lean.Core.Context → Lean.Syntax
-- Mathlib.Data.PNat.Factors
/-- Lists can be coerced to multisets; here we have some results
about how this interacts with our constructions on multisets.  -/
PrimeMultiset.ofNatList : (l : List ℕ) → (∀ p ∈ l, Nat.Prime p) → PrimeMultiset
-- Mathlib.LinearAlgebra.RootSystem.Chain
RootPairing.coe_chainBotCoeff_eq_sSup : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : CharZero R] [inst_3 : IsDomain R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsCrystallographic] {i j : ι},
  LinearIndependent R ![P.root i, P.root j] →
    ↑(RootPairing.chainBotCoeff i j) = sSup {k | P.root j - k • P.root i ∈ Set.range ⇑P.root}
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
CategoryTheory.OrthogonalReflection.reflectionObj.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W W_1 : CategoryTheory.MorphismProperty C) (e_W : W = W_1)
  (Z Z_1 : C),
  Z = Z_1 →
    ∀ [inst_1 : CategoryTheory.Limits.HasPushouts C]
      [inst_2 : ∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁]
      [inst_3 : ∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂]
      [inst_4 :
        ∀ (Z : C),
          CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)]
      (κ : Cardinal.{w}) [inst_5 : OrderBot κ.ord.ToType]
      [inst_6 : CategoryTheory.Limits.HasIterationOfShape κ.ord.ToType C],
      CategoryTheory.OrthogonalReflection.reflectionObj W Z κ =
        CategoryTheory.OrthogonalReflection.reflectionObj W_1 Z_1 κ
-- Std.Do.Triple.SpecLemmas
MonadState.set.eq_1 : ∀ {σ : Type u} (m : Type u → Type v) [self : MonadState σ m], MonadState.set = self.2
-- Mathlib.Combinatorics.SimpleGraph.StronglyRegular
SimpleGraph.IsSRGWith.card_neighborFinset_union_eq : ∀ {V : Type u} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] {n k ℓ μ : ℕ}
  [inst_2 : DecidableEq V] {v w : V},
  G.IsSRGWith n k ℓ μ → (G.neighborFinset v ∪ G.neighborFinset w).card = 2 * k - Fintype.card ↑(G.commonNeighbors v w)
-- Mathlib.AlgebraicGeometry.OrderOfVanishing
/-- The order of vanishing of an element of the function field of a locally Noetherian integral scheme
at a point. This has a junk value of `0` if `f = 0` or if `coheight z ≠ 1`.
 -/
AlgebraicGeometry.Scheme.ord : {X : AlgebraicGeometry.Scheme} →
  [inst : AlgebraicGeometry.IsIntegral X] → [AlgebraicGeometry.IsLocallyNoetherian X] → ↑X.functionField → ↥X → ℤ
-- Batteries.Data.Vector.Lemmas
Vector.toArray_scanr : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {init : β} {f : α → β → β} {as : Vector α n},
  (Vector.scanr f init as).toArray = Array.scanr f init as.toArray
-- Mathlib.RingTheory.LocalProperties.Basic
RingHom.ofLocalizationSpan_iff_finite : ∀ (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop),
  RingHom.OfLocalizationSpan P ↔ RingHom.OfLocalizationFiniteSpan P
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
NumberField.mixedEmbedding.convexBodyLT_convex : ∀ (K : Type u_1) [inst : Field K] (f : NumberField.InfinitePlace K → NNReal),
  Convex ℝ (NumberField.mixedEmbedding.convexBodyLT K f)
-- Mathlib.CategoryTheory.Abelian.SerreClass.Localization
CategoryTheory.ObjectProperty.exists_comp_monoModSerre_eq_zero_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsSerreClass] {X Y : C} (f : X ⟶ Y),
  (∃ Y' s, ∃ (_ : P.monoModSerre s), CategoryTheory.CategoryStruct.comp f s = 0) ↔ P (CategoryTheory.Abelian.image f)
-- Batteries.Data.List.Lemmas
/-- **Alias** of `List.IsChain.cons_of_imp_of_imp`. -/
List.Chain.imp' : ∀ {α : Type u_1} {R S : α → α → Prop} {a : α} {l : List α} {b : α},
  (∀ ⦃a b : α⦄, R a b → S a b) → (∀ ⦃c : α⦄, R a c → S b c) → List.IsChain R (a :: l) → List.IsChain S (b :: l)
-- Std.Data.DTreeMap.Internal.Model
Ordering.swap.eq_1 : Ordering.lt.swap = Ordering.gt
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
SSet.normalizedChainComplex_hom_ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] {X : SSet} {R : C} {n : ℕ} {T : C}
  {f g : (X.normalizedChainComplex R).X n ⟶ T},
  f = g ↔
    ∀ x ∈ X.nonDegenerate n,
      CategoryTheory.CategoryStruct.comp (X.ιNormalizedChainComplex x) f =
        CategoryTheory.CategoryStruct.comp (X.ιNormalizedChainComplex x) g
-- Mathlib.Data.Int.Cast.Defs
AddGroupWithOne.zsmul_succ' : ∀ {R : Type u} [self : AddGroupWithOne R] (n : ℕ) (a : R), ↑n.succ • a = ↑n • a + a
-- Init.Internal.Order.While
_private.Init.Internal.Order.While.0.Lean.Loop.forIn.match_1.splitter : {β : Type u_1} →
  (motive : ForInStep β → Sort u_2) →
    (__do_lift : ForInStep β) →
      ((b' : β) → motive (ForInStep.done b')) → ((b' : β) → motive (ForInStep.yield b')) → motive __do_lift
-- Mathlib.Analysis.Normed.Group.Constructions
OrderDual.seminormedAddGroup.eq_1 : ∀ {E : Type u_2} [inst : SeminormedAddGroup E],
  OrderDual.seminormedAddGroup =
    { toNorm := OrderDual.toNorm, toAddGroup := OrderDual.instAddGroup,
      toPseudoMetricSpace := instPseudoMetricSpaceOrderDual, dist_eq := ⋯ }
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
FractionalIdeal.inv_le_comm : ∀ {A : Type u_2} {K : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : IsDedekindDomain A]
  [inst_3 : Algebra A K] [inst_4 : IsFractionRing A K] {I J : FractionalIdeal (nonZeroDivisors A) K},
  I ≠ 0 → J ≠ 0 → (I⁻¹ ≤ J ↔ J⁻¹ ≤ I)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multiequalizer.multifork_π_app_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) [inst_1 : CategoryTheory.Limits.HasMultiequalizer I] (a : J.L),
  (CategoryTheory.Limits.Multiequalizer.multifork I).π.app (CategoryTheory.Limits.WalkingMulticospan.left a) =
    CategoryTheory.Limits.Multiequalizer.ι I a
-- Mathlib.Algebra.CharZero.Defs
Nat.cast_ne_zero : ∀ {R : Type u_1} [inst : AddMonoidWithOne R] [CharZero R] {n : ℕ}, ↑n ≠ 0 ↔ n ≠ 0
-- Mathlib.CategoryTheory.Functor.FullyFaithful
/-- If `F` is fully faithful and `F ≅ G`, then `G` is fully faithful.  -/
CategoryTheory.Functor.FullyFaithful.ofIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          F.FullyFaithful → {G : CategoryTheory.Functor C D} → (F ≅ G) → G.FullyFaithful
-- Mathlib.GroupTheory.ArchimedeanDensely
/-- **Alias** of `LinearOrderedCommGroupWithZero.wellFoundedOn_setOfPred_le_lt_iff_nonempty_discrete_of_ne_zero`. -/
LinearOrderedCommGroupWithZero.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete_of_ne_zero : ∀ {G₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero G₀] [Nontrivial G₀ˣ] {g : G₀},
  g ≠ 0 → (({x | g ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2) ↔ Nonempty (G₀ ≃*o WithZero (Multiplicative ℤ)))
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
WithTop.sSup_singleton_top : ∀ {α : Type u_1} [inst : LE α] [inst_1 : SupSet α], sSup {⊤} = ⊤