mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Abelian.Projective.Ext
CategoryTheory.ProjectiveResolution.extAddEquivCohomologyClass_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (R : CategoryTheory.ProjectiveResolution X) {n : ℕ}
  (a : CategoryTheory.Abelian.Ext X Y n), R.extAddEquivCohomologyClass a = R.extEquivCohomologyClass a
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get?_eq_some_get!_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β] {a : α}, t.contains a = true → Std.DTreeMap.Const.get? t a = some (Std.DTreeMap.Const.get! t a)
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.symm_trans_self : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂), e.symm.trans e = AlgEquiv.refl
-- Mathlib.RingTheory.Idempotents
OrthogonalIdempotents.ortho : ∀ {R : Type u_1} [inst : Semiring R] {I : Type u_3} {e : I → R},
  OrthogonalIdempotents e → Pairwise fun x1 x2 => e x1 * e x2 = 0
-- Mathlib.Algebra.Polynomial.Eval.Degree
Polynomial.eval₂_eq_sum_range' : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) {p : Polynomial R} {n : ℕ},
  p.natDegree < n → ∀ (x : S), Polynomial.eval₂ f x p = ∑ i ∈ Finset.range n, f (p.coeff i) * x ^ i
-- Lean.Elab.Tactic.Split
_private.Lean.Elab.Tactic.Split.0.Lean.Elab.Tactic.evalSplit.throwMultipleLocationsAt : Lean.Syntax → Bool → Array Lean.Syntax → {α : Type} → Lean.MetaM α
-- Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
ExteriorAlgebra.liftAlternating_algebraMap : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (r : R),
  (ExteriorAlgebra.liftAlternating f) ((algebraMap R (ExteriorAlgebra R M)) r) = r • (f 0) 0
-- Mathlib.Analysis.Normed.Group.Real
Real.enorm_toReal : ∀ {a : ENNReal}, a ≠ ⊤ → ‖a.toReal‖ₑ = a
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.two_mul_arctan : ∀ {x : ℝ}, -1 < x → x < 1 → 2 * Real.arctan x = Real.arctan (2 * x / (1 - x ^ 2))
-- Mathlib.Data.List.Fold
/-- **Alias** of `List.foldr_cons_eq_foldr_apply`. -/
List.foldr_eq_of_comm' : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : α → β → β} {a : α} {b : β} [hf : LeftCommutative f],
  List.foldr f b (a :: l) = List.foldr f (f a b) l
-- Mathlib.Topology.NhdsSet
nhdsSet_mono : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s t : Set X}, s ⊆ t → nhdsSet s ≤ nhdsSet t
-- Mathlib.Data.Matrix.Mul
Matrix.mulVec_transpose : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalCommSemiring α] [inst_1 : Fintype m] (A : Matrix m n α)
  (x : m → α), A.transpose.mulVec x = Matrix.vecMul x A
-- Mathlib.Algebra.Group.End
MulAut.conj_symm_apply : ∀ {G : Type u_3} [inst : Group G] (g h : G), (MulEquiv.symm (MulAut.conj g)) h = g⁻¹ * h * g
-- Mathlib.Topology.Category.TopCat.Limits.Pullbacks
TopCat.pullbackIsoProdSubtype_inv_fst : ∀ {X Y Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (TopCat.pullbackIsoProdSubtype f g).inv (CategoryTheory.Limits.pullback.fst f g) =
    TopCat.pullbackFst f g
-- Mathlib.Probability.Moments.Variance
/-- **Popoviciu's inequality on variances**

The variance of a random variable `X` satisfying `a ≤ X ≤ b` almost everywhere is at most
`((b - a) / 2) ^ 2`.  -/
ProbabilityTheory.variance_le_sq_of_bounded : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {a b : ℝ}
  {X : Ω → ℝ},
  (∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b) → AEMeasurable X μ → ProbabilityTheory.variance X μ ≤ ((b - a) / 2) ^ 2
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ D` reflects finite colimits, then `F.op : Cᵒᵖ ⥤ Dᵒᵖ` reflects finite
limits.  -/
CategoryTheory.Limits.reflectsFiniteLimits_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsFiniteColimits F],
  CategoryTheory.Limits.ReflectsFiniteLimits F.op
-- Mathlib.Analysis.Normed.Group.Basic
nnnorm_inv' : ∀ {E : Type u_5} [inst : SeminormedGroup E] (a : E), ‖a⁻¹‖₊ = ‖a‖₊
-- Mathlib.Topology.Algebra.Group.Quotient
/-- Neighborhoods in the quotient are precisely the map of neighborhoods in the prequotient.  -/
QuotientAddGroup.nhds_eq : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [SeparatelyContinuousAdd G] (N : AddSubgroup G)
  (x : G), nhds ↑x = Filter.map QuotientAddGroup.mk (nhds x)
-- Init.Core
/-- Lexicographical order for products.

Two pairs are lexicographically ordered if their first elements are ordered or if their first
elements are equal and their second elements are ordered.
 -/
Prod.lexLt : {α : Type u_1} → {β : Type u_2} → [LT α] → [LT β] → α × β → α × β → Prop
-- Init.Coe
/-- Auxiliary class implementing `CoeHead* Coe* CoeTail?`.
Users should generally not implement this directly.
 -/
CoeHTCT : Sort u → Sort v → Sort (max (max 1 u) v)
-- Mathlib.RingTheory.Multiplicity
multiplicity_ne_zero : ∀ {α : Type u_1} [inst : Monoid α] {a b : α}, multiplicity a b ≠ 0 ↔ a ∣ b
-- Mathlib.CategoryTheory.EssentiallySmall
/-- Constructor for `EssentiallySmall C` from an explicit small category witness.  -/
CategoryTheory.EssentiallySmall.mk' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : Type w} [inst_1 : CategoryTheory.SmallCategory S]
  (e : C ≌ S), CategoryTheory.EssentiallySmall.{w, v, u} C
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.CoGrothendieck.ext_iff : ∀ {𝒮 : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} 𝒮}
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} {x y : F.CoGrothendieck},
  x = y ↔ x.base = y.base ∧ x.fiber ≍ y.fiber
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.map_verts : ∀ {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (H : G.Subgraph),
  (SimpleGraph.Subgraph.map f H).verts = ⇑f '' H.verts
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rii.eq_succMany?_of_toArray_eq_append_append : ∀ {α : Type u} {r : Std.Rii α} [inst : Std.PRange.Least? α] [inst_1 : Std.PRange.UpwardEnumerable α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] [inst_3 : Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_4 : Std.Rxi.IsAlwaysFinite α] {pref suff : Array α} {cur : α} (h : r.toArray = pref ++ #[cur] ++ suff),
  cur = (Std.PRange.least?.bind (Std.PRange.succMany? pref.size)).get ⋯
-- Mathlib.Topology.Algebra.Constructions
/-- `MulOpposite.op` as a homeomorphism.  -/
MulOpposite.opHomeomorph : {M : Type u_1} → [inst : TopologicalSpace M] → M ≃ₜ Mᵐᵒᵖ
-- Mathlib.LinearAlgebra.Pi
LinearMap.disjoint_single_single : ∀ (R : Type u) {ι : Type x} [inst : Semiring R] (φ : ι → Type i) [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)] [inst_3 : DecidableEq ι] (I J : Set ι),
  Disjoint I J → Disjoint (⨆ i ∈ I, (LinearMap.single R φ i).range) (⨆ i ∈ J, (LinearMap.single R φ i).range)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.instFullGrpFunctorOppositeGrpCatYonedaGrp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.yonedaGrp.Full
-- Mathlib.FieldTheory.Finite.Basic
FiniteField.card_cast_subgroup_card_ne_zero : ∀ {K : Type u_1} [inst : Ring K] [NoZeroDivisors K] [Nontrivial K] (G : Subgroup Kˣ) [inst_3 : Fintype ↥G],
  ↑(Fintype.card ↥G) ≠ 0
-- Mathlib.SetTheory.Ordinal.FundamentalSequence
Ordinal.IsFundamentalSequence.eq_1 : ∀ (a o : Ordinal.{u}) (f : (b : Ordinal.{u}) → b < o → Ordinal.{u}),
  a.IsFundamentalSequence o f =
    (o ≤ a.cof.ord ∧ (∀ {i j : Ordinal.{u}} (hi : i < o) (hj : j < o), i < j → f i hi < f j hj) ∧ o.blsub f = a)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.isEmpty_empty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}, ∅.isEmpty = true
-- Init.Data.List.Find
List.finIdxOf?.eq_1 : ∀ {α : Type u} [inst : BEq α] (a : α), List.finIdxOf? a = List.findFinIdx? fun x => x == a
-- Mathlib.Geometry.Euclidean.Altitude
Affine.Simplex.height.congr_simp : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s s_1 : Affine.Simplex ℝ P n),
  s = s_1 → ∀ (i i_1 : Fin (n + 1)), i = i_1 → s.height i = s_1.height i_1
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
Int.reduceBEq : Lean.Meta.Simp.DSimproc
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.E₆_off_diag_nonpos : ∀ (i j : Fin 6), i ≠ j → CartanMatrix.E₆ i j ≤ 0
-- Init.Core
Quot.inductionOn : ∀ {α : Sort u} {r : α → α → Prop} {motive : Quot r → Prop} (q : Quot r), (∀ (a : α), motive (Quot.mk r a)) → motive q
-- Mathlib.RingTheory.Localization.Basic
/-- For an algebra isomorphism `f : A ≃ₐ[R] B`, if `A` and `B` are algebras over a localization
`S` of `R`, then `f` is automatically an `S`-algebra isomorphism.  -/
AlgEquiv.extendScalarsOfIsLocalization : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] →
            (S : Type u_4) →
              [inst_3 : CommSemiring S] →
                [inst_4 : Algebra R S] →
                  (M : Submonoid R) →
                    [IsLocalization M S] →
                      [inst_6 : Algebra R A] →
                        [inst_7 : Algebra S A] →
                          [IsScalarTower R S A] →
                            [inst_9 : Algebra R B] →
                              [inst_10 : Algebra S B] → [IsScalarTower R S B] → (A ≃ₐ[R] B) → A ≃ₐ[S] B
-- Mathlib.CategoryTheory.Monoidal.Action.End
CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionAssocIso_inv : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)ᴹᵒᵖ) [inst_3 : F.Monoidal] (c c' : C) (d : D),
  (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c' d).inv =
    (CategoryTheory.Functor.LaxMonoidal.μ F c c').unmop.app d
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.instToFormatIProp : Std.ToFormat Mathlib.Tactic.ITauto.IProp
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.map_addU : ∀ {F : Type u} {K : Type v} [inst : Field F] [inst_1 : Field K] (f : F →+* K) (P Q : Fin 3 → F),
  WeierstrassCurve.Projective.addU (⇑f ∘ P) (⇑f ∘ Q) = f (WeierstrassCurve.Projective.addU P Q)
-- Mathlib.Algebra.Category.Ring.Basic
CommRingCat.hasForgetToRingCat : CategoryTheory.HasForget₂ CommRingCat RingCat
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
/-- The lattice spanned by a pair of periods.  -/
PeriodPair.lattice : PeriodPair → Submodule ℤ ℂ
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonCallHierarchyOutgoingCall : Lean.FromJson Lean.Lsp.CallHierarchyOutgoingCall
-- Mathlib.RingTheory.DedekindDomain.SelmerGroup
IsDedekindDomain.selmerGroup.fromUnit_ker : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type v} [inst_2 : Field K] [inst_3 : Algebra R K]
  [inst_4 : IsFractionRing R K] {n : ℕ} [hn : Fact (0 < n)],
  IsDedekindDomain.selmerGroup.fromUnit.ker = (powMonoidHom n).range
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasProdLocallyUniformly.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] (f : ι → β → α) (g : β → α)
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β],
  HasProdLocallyUniformly f g = TendstoLocallyUniformly (fun x1 x2 => ∏ i ∈ x1, f i x2) g Filter.atTop
-- Mathlib.Probability.Process.Adapted
MeasureTheory.Adapted.neg : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : ι → Type u_3} [inst_1 : (i : ι) → MeasurableSpace (β i)] {u : (i : ι) → Ω → β i}
  [inst_2 : (i : ι) → AddGroup (β i)] [∀ (i : ι), MeasurableNeg (β i)],
  MeasureTheory.Adapted f u → MeasureTheory.Adapted f (-u)
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.det_units_conj : ∀ {m : Type u_1} [inst : DecidableEq m] [inst_1 : Fintype m] {R : Type v} [inst_2 : CommRing R] (M : (Matrix m m R)ˣ)
  (N : Matrix m m R), (↑M * N * ↑M⁻¹).det = N.det
-- Mathlib.Order.Filter.Pointwise
Filter.covariant_smul : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β],
  CovariantClass (Filter α) (Filter β) (fun x1 x2 => x1 • x2) fun x1 x2 => x1 ≤ x2
-- Mathlib.Analysis.InnerProductSpace.SingularValues
LinearMap.singularValues_eq_zero_iff : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E] {F : Type u_3} [inst_4 : NormedAddCommGroup F] [inst_5 : InnerProductSpace 𝕜 F]
  [inst_6 : FiniteDimensional 𝕜 F] (T : E →ₗ[𝕜] F), T.singularValues = 0 ↔ T = 0
-- Mathlib.Tactic.Algebra.Basic
Mathlib.Tactic.Algebra.BaseType.mk : {u v : Lean.Level} →
  {R : Q(Type u)} →
    {A : Q(Type v)} →
      {sR : Q(CommSemiring «$R»)} →
        {sA : Q(CommSemiring «$A»)} →
          {sAlg : Q(Algebra «$R» «$A»)} →
            (r : Q(«$R»)) →
              Mathlib.Tactic.Ring.ExSum q(«$sR») r → Mathlib.Tactic.Algebra.BaseType sAlg q((algebraMap «$R» «$A») «$r»)
-- Init.Data.String.Pattern.Char
String.Slice.Pattern.Char.instLawfulBackwardPatternChar : ∀ {c : Char}, String.Slice.Pattern.LawfulBackwardPattern c
-- Init.Data.Array.FinRange
Array.finRange_succ : ∀ {n : ℕ}, Array.finRange (n + 1) = #[0] ++ Array.map Fin.succ (Array.finRange n)
-- Mathlib.RingTheory.SimpleModule.Basic
RingHom.isSemisimpleRing_of_surjective : ∀ {R : Type u_2} {S : Type u_3} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S),
  Function.Surjective ⇑f → ∀ [IsSemisimpleRing R], IsSemisimpleRing S
-- Init.Data.Nat.Basic
Nat.pred_eq_sub_one : ∀ {n : ℕ}, n.pred = n - 1
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.ofLp_surjective : ∀ (p : ENNReal) {V : Type u_4}, Function.Surjective WithLp.ofLp
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instIsLeftCancelMul : ∀ {α : Type u_1} [inst : Mul α] [IsLeftCancelMul α], IsLeftCancelMul (Colex α)
-- Mathlib.Analysis.Convex.Integral
/-- If `μ` is a non-zero finite measure on `α`, `s` is a convex closed set in `E`, and `f` is an
integrable function sending `μ`-a.e. points to `s`, then the average value of `f` belongs to `s`:
`⨍ x, f x ∂μ ∈ s`. See also `Convex.centerMass_mem` for a finite sum version of this lemma.  -/
Convex.average_mem : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {f : α → E} [MeasureTheory.IsFiniteMeasure μ] [NeZero μ],
  Convex ℝ s → IsClosed s → (∀ᵐ (x : α) ∂μ, f x ∈ s) → MeasureTheory.Integrable f μ → ⨍ (x : α), f x ∂μ ∈ s
-- Mathlib.Algebra.Group.Subsemigroup.Membership
Subsemigroup.mul_mem_sup : ∀ {M : Type u_2} [inst : Mul M] {S T : Subsemigroup M} {x y : M}, x ∈ S → y ∈ T → x * y ∈ S ⊔ T
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.open_baseSet : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace Z] {proj : Z → B} (self : Bundle.Trivialization F proj), IsOpen self.baseSet
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.mem_sInf : ∀ {G : Type u_1} [inst : Group G] {S : Set (Subgroup G)} {x : G}, x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p
-- Mathlib.Algebra.Order.Group.PosPart
mabs_mul_eq_oneLePart_sq : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : CommGroup α] [MulLeftMono α] (a : α), |a|ₘ * a = a⁺ᵐ ^ 2
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.degree_add_degree_leadingCoeff_inv : ∀ {K : Type u_1} [inst : DivisionRing K] (p : Polynomial K),
  p.degree + (Polynomial.C p.leadingCoeff⁻¹).degree = p.degree
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Run `grind +suggestions` at every step in proofs, reporting where it succeeds.  -/
tryAtEachStepGrindSuggestions : Mathlib.TacticAnalysis.Config
-- Mathlib.SetTheory.ZFC.Class
Class.coe_mem : ∀ {x : ZFSet.{u}} {A : Class.{u}}, ↑x ∈ A ↔ A x
-- Mathlib.Combinatorics.SimpleGraph.Basic
/-- This lemma, combined with `edgeSet_sdiff` and `edgeSet_fromEdgeSet`,
allows proving `(G \ fromEdgeSet s).edgeSet = G.edgeSet \ s` by `simp`.  -/
SimpleGraph.edgeSet_sdiff_sdiff_isDiag : ∀ {V : Type u} (G : SimpleGraph V) (s : Set (Sym2 V)), G.edgeSet \ (s \ Sym2.diagSet) = G.edgeSet \ s
-- Std.Internal.Do.WP.Basic
/-- `OptionT`'s `WP` interpretation: lift the base interpretation by adding a `PUnit` exception
postcondition layer.  -/
Std.Internal.Do.OptionT.wpInst : {m : Type u → Type z} →
  {EPred : Type u_1} →
    {α Pred : Type u} →
      [inst : Std.Internal.Do.Assertion Pred] →
        [inst_1 : Std.Internal.Do.Assertion EPred] →
          [Std.Internal.Do.WP (m (Option α)) (Option α) Pred EPred] →
            Std.Internal.Do.WP (OptionT m α) α Pred (EPost.Cons✝ Pred EPred)
-- Mathlib.CategoryTheory.Products.Unitor
CategoryTheory.prod.rightUnitor_isEquivalence : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C], (CategoryTheory.prod.rightUnitor C).IsEquivalence
-- Mathlib.FieldTheory.RatFunc.Basic
/-- `K⟮X⟯` is an additive commutative group.

This is an intermediate step on the way to the full instance `RatFunc.instCommRing`.
 -/
RatFunc.instAddCommGroup : (K : Type u) → [inst : CommRing K] → AddCommGroup (RatFunc K)
-- Mathlib.Data.Nat.MaxPowDiv
padicValNat_zero_right : ∀ (p : ℕ), padicValNat p 0 = 0
-- Mathlib.CategoryTheory.Limits.Creates
CategoryTheory.CreatesLimit.toReflectsLimit : ∀ {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} {K : CategoryTheory.Functor J C}
  {F : CategoryTheory.Functor C D} [self : CategoryTheory.CreatesLimit K F], CategoryTheory.Limits.ReflectsLimit K F
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.closure.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] (k : Set G), AddSubgroup.closure k = sInf {K | k ⊆ ↑K}
-- Mathlib.RepresentationTheory.Coinduced
Rep.coindFunctor'_map : ∀ (k : Type u) {G : Type v} {H : Type w} [inst : CommRing k] [inst_1 : Monoid G] [inst_2 : Monoid H] (φ : G →* H)
  {X Y : Rep.{max u w, u, v} k G} (f : X ⟶ Y), (Rep.coindFunctor' k φ).map f = Rep.coindMap' φ f
-- Std.Data.HashSet.Lemmas
Std.HashSet.toList_toArray : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α}, m.toArray.toList = m.toList
-- Mathlib.Algebra.Order.Ring.Ordering.Basic
RingPreordering.unitsInv_mem : ∀ {R : Type u_1} [inst : CommRing R] {P : RingPreordering R} {a : Rˣ}, ↑a ∈ P → ↑a⁻¹ ∈ P
-- Mathlib.Analysis.Calculus.Deriv.Basic
HasDerivAtFilter.isBigO_sub_rev : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {L : Filter (𝕜 × 𝕜)},
  HasDerivAtFilter f f' L → f' ≠ 0 → (fun p => p.1 - p.2) =O[L] fun p => f p.1 - f p.2
-- Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
/-- An ordered monoid with one-sided 'division' in the sense that
if `a ≤ b`, there is some `c` for which `a * c = b`. This is a weaker version
of the condition on canonical orderings defined by `CanonicallyOrderedMul`.  -/
ExistsMulOfLE : (α : Type u) → [Mul α] → [LE α] → Prop
-- Init.Data.Array.InsertIdx
Array.getElem?_insertIdx_of_ge : ∀ {α : Type u} {xs : Array α} {x : α} {i k : ℕ} (w : i < k) (h : k ≤ xs.size), (xs.insertIdx i x ⋯)[k]? = xs[k - 1]?
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
Real.sSup_univ : sSup Set.univ = 0
-- Mathlib.Topology.MetricSpace.Sequences
/-- A version of **Bolzano-Weierstrass**: in a proper metric space (e.g. $ℝ^n$),
every bounded sequence has a converging subsequence.  -/
tendsto_subseq_of_bounded : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] [ProperSpace X] {s : Set X},
  Bornology.IsBounded s →
    ∀ {x : ℕ → X},
      (∀ (n : ℕ), x n ∈ s) → ∃ a ∈ closure s, ∃ φ, StrictMono φ ∧ Filter.Tendsto (x ∘ φ) Filter.atTop (nhds a)
-- Init.Data.Array.Lemmas
Array.singleton_eq_append_iff : ∀ {α : Type u_1} {xs ys : Array α} {x : α}, #[x] = xs ++ ys ↔ xs = #[] ∧ ys = #[x] ∨ xs = #[x] ∧ ys = #[]
-- Mathlib.Algebra.Polynomial.Smeval
Polynomial.smeval_X_pow : ∀ (R : Type u_1) [inst : Semiring R] {S : Type u_2} [inst_1 : AddCommMonoid S] [inst_2 : Pow S ℕ]
  [inst_3 : MulActionWithZero R S] (x : S) {n : ℕ}, (Polynomial.X ^ n).smeval x = x ^ n
-- Mathlib.NumberTheory.Fermat
/-- Prime `a ^ n + 1` implies `n` is a power of two (**Fermat primes**).  -/
Nat.pow_of_pow_add_prime : ∀ {a n : ℕ}, 1 < a → n ≠ 0 → Nat.Prime (a ^ n + 1) → ∃ m, n = 2 ^ m
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.reverse_injective : ∀ {n : ℕ}, Function.Injective Composition.reverse
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_preimage_of_subset_range : ∀ {α β : Type u} (f : α → β), ∀ s ⊆ Set.range f, Cardinal.mk ↑s ≤ Cardinal.mk ↑(f ⁻¹' s)
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.SimpleFunc.setToSimpleFunc_congr : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (T : Set α → E →L[ℝ] F),
  (∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0) →
    MeasureTheory.FinMeasAdditive μ T →
      ∀ {f g : MeasureTheory.SimpleFunc α E},
        MeasureTheory.Integrable (⇑f) μ →
          ⇑f =ᵐ[μ] ⇑g → MeasureTheory.SimpleFunc.setToSimpleFunc T f = MeasureTheory.SimpleFunc.setToSimpleFunc T g
-- Mathlib.Topology.Subpath
/-- Alternative to `Path.Homotopy.concatHcomp` in terms of `Path.Homotopic`.  -/
Path.Homotopic.concat_hcomp : ∀ {X : Type u_1} [inst : TopologicalSpace X] {n : ℕ} (p : Fin (n + 1) → X)
  (F G : (k : Fin n) → Path (p k.castSucc) (p k.succ)),
  (∀ (k : Fin n), (F k).Homotopic (G k)) → (Path.concat p F).Homotopic (Path.concat p G)
-- Mathlib.Order.OrderDual
OrderDual.forall : ∀ {α : Type u_1} {p : αᵒᵈ → Prop}, (∀ (a : αᵒᵈ), p a) ↔ ∀ (a : α), p (OrderDual.toDual a)
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
add_add_tsub_cancel : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α], c ≤ b → a + c + (b - c) = a + b
-- Mathlib.Algebra.Order.Group.PosPart
maxDefault.eq_1 : ∀ {α : Type u_1} [inst : LE α] [inst_1 : DecidableLE α] (a b : α), maxDefault a b = if a ≤ b then b else a
-- Mathlib.Algebra.Homology.HomologySequence
HomologicalComplex.opcyclesToCycles_naturality_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c} (φ : K ⟶ L)
  (i j : ι) [inst_2 : K.HasHomology i] [inst_3 : K.HasHomology j] [inst_4 : L.HasHomology i] [inst_5 : L.HasHomology j]
  {Z : C} (h : L.cycles j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap φ i)
      (CategoryTheory.CategoryStruct.comp (L.opcyclesToCycles i j) h) =
    CategoryTheory.CategoryStruct.comp (K.opcyclesToCycles i j)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap φ j) h)
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_nonpos_of_nonneg_of_nonpos : ∀ {a b : ℤ}, 0 ≤ a → b ≤ 0 → a / b ≤ 0
-- Mathlib.Data.Finset.Filter
Finset.filter_comm : ∀ {α : Type u_1} (p q : α → Prop) [inst : DecidablePred p] [inst_1 : DecidablePred q] (s : Finset α),
  Finset.filter q (Finset.filter p s) = Finset.filter p (Finset.filter q s)
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.hasAltRHS : Lean.Syntax → Bool