mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Nat.Lemmas
Nat.max_right_comm : ∀ (a b c : ℕ), max (max a b) c = max (max a c) b
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.instIsLocalization : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : CommSemiring R] {S : Type u_4}
  [inst_2 : CommRing S] [inst_3 : Algebra R S] (M : Submonoid R) [IsLocalization M S] (v : Valuation S Γ₀),
  IsLocalization M (WithVal v)
-- Std.Data.String.ToNat
String.Slice.isNat_iff : ∀ {s : String.Slice},
  s.isNat = true ↔
    s.isEmpty = false ∧
      (∀ c ∈ s.copy.toList, c.isDigit = true ∨ c = '_') ∧
        ¬['_', '_'] <:+: s.copy.toList ∧ s.copy.toList.head? ≠ some '_' ∧ s.copy.toList.getLast? ≠ some '_'
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.coeFnAddMonoidHom_apply : ∀ {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] (v : DirectSum ι fun i => β i),
  (DirectSum.coeFnAddMonoidHom β) v = ⇑v
-- Mathlib.Data.QPF.Multivariate.Constructions.Sigma
_private.Mathlib.Data.QPF.Multivariate.Constructions.Sigma.0.MvQPF.Sigma.abs.match_1.splitter : {n : ℕ} →
  {A : Type u_1} →
    (F : A → TypeVec.{u_1} n → Type u_1) →
      [inst : (α : A) → MvQPF (F α)] →
        ⦃α : TypeVec.{u_1} n⦄ →
          (motive : ↑(MvQPF.Sigma.P F) α → Sort u_2) →
            (x : ↑(MvQPF.Sigma.P F) α) →
              ((a : (MvQPF.Sigma.P F).A) → (f : ((MvQPF.Sigma.P F).B a).Arrow α) → motive ⟨a, f⟩) → motive x
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.Γ'.fintype : {K : Type u_1} →
  {Γ : K → Type u_2} → [DecidableEq K] → [Fintype K] → [(k : K) → Fintype (Γ k)] → Fintype (Turing.TM2to1.Γ' K Γ)
-- Mathlib.NumberTheory.LSeries.RiemannZeta
/-- Riemann zeta functional equation, formulated for `Λ₀`: for any complex `s` we have
`Λ₀(1 - s) = Λ₀ s`.  -/
completedRiemannZeta₀_one_sub : ∀ (s : ℂ), completedRiemannZeta₀ (1 - s) = completedRiemannZeta₀ s
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.twoTorsionPolynomial_discr_ne_zero_of_isElliptic : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] [Nontrivial R],
  IsUnit 2 → W.twoTorsionPolynomial.discr ≠ 0
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.LeftExtension.whiskering_map : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {x : B} (h : c ⟶ x)
  {X Y : CategoryTheory.Bicategory.LeftExtension f g} (η : X ⟶ Y),
  (CategoryTheory.Bicategory.LeftExtension.whiskering h).map η =
    CategoryTheory.Bicategory.LeftExtension.homMk
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.StructuredArrow.Hom.right η) h) ⋯
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.instSub : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : AddGroup β] → [IsTopologicalAddGroup β] → Sub (CompactlySupportedContinuousMap α β)
-- Mathlib.Analysis.Polynomial.Fourier
/-- **Parseval's Identity** for polynomials  -/
Polynomial.sum_sq_norm_coeff_eq_circleAverage : ∀ (p : Polynomial ℂ), ∑ i ∈ p.support, ‖p.coeff i‖ ^ 2 = Real.circleAverage (fun θ => ‖Polynomial.eval θ p‖ ^ 2) 0 1
-- Std.Time.Zoned.RecurringRule
Std.Time.TimeZone.TransitionSpec.julian.sizeOf_spec : ∀ (day : Std.Time.Internal.Bounded.LE 1 365), sizeOf (Std.Time.TimeZone.TransitionSpec.julian day) = 1 + sizeOf day
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.isUnit_comp : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) (j : N →* P) (y : ↥S), IsUnit ((j.comp f.toMonoidHom) ↑y)
-- Mathlib.ModelTheory.ElementaryMaps
/-- The underlying embedding  -/
FirstOrder.Language.ElementaryEmbedding.toFun : {L : FirstOrder.Language} →
  {M : Type u_1} →
    {N : Type u_2} → [inst : L.Structure M] → [inst_1 : L.Structure N] → L.ElementaryEmbedding M N → M → N
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
/-- Let `f, g` be monic polynomials over `K`. If `f` is irreducible, and `g(x) - α` is irreducible
in `K⟮α⟯` with `α` a root of `f`, then `f(g(x))` is irreducible.  -/
Polynomial.irreducible_comp : ∀ {K : Type u} [inst : Field K] {f g : Polynomial K},
  f.Monic →
    g.Monic →
      Irreducible f →
        (∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
            minpoly K x = f →
              Irreducible
                (Polynomial.map (algebraMap K ↥K⟮x⟯) g - Polynomial.C (IntermediateField.AdjoinSimple.gen K x))) →
          Irreducible (f.comp g)
-- Mathlib.Data.Int.Star
Int.addSubmonoid_closure_range_pow : ∀ {n : ℕ}, Even n → AddSubmonoid.closure (Set.range fun x => x ^ n) = AddSubmonoid.nonneg ℤ
-- Mathlib.Analysis.Normed.Operator.Basic
LinearIsometry.toSpanSingleton_apply : ∀ {𝕜 : Type u_1} {E : Type u_4} [inst : SeminormedAddCommGroup E] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NormedSpace 𝕜 E] {v : E} (hv : ‖v‖ = 1) (a : 𝕜), (LinearIsometry.toSpanSingleton 𝕜 E hv) a = a • v
-- Init.Data.Order.Ord
Std.TransCmp.opposite : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp], Std.TransCmp fun a b => cmp b a
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
nnnorm_cfc_lt : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [inst : RCLike 𝕜] [inst_1 : NormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedAlgebra 𝕜 A] [inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p] {f : 𝕜 → 𝕜}
  {a : A} {c : NNReal}, 0 < c → (∀ x ∈ spectrum 𝕜 a, ‖f x‖₊ < c) → ‖cfc f a‖₊ < c
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.left_cancel_posSubmonoid : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] (x y : R) (u : ↥(ValuativeRel.posSubmonoid R)),
  ↑u * x ≤ᵥ ↑u * y ↔ x ≤ᵥ y
-- Mathlib.Topology.Algebra.Order.Archimedean
/-- A subgroup of an archimedean linear ordered multiplicative commutative group `G` with order
topology either is dense in `G` or is a cyclic subgroup.  -/
Subgroup.dense_or_cyclic : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] [inst_3 : TopologicalSpace G]
  [OrderTopology G] [MulArchimedean G] (S : Subgroup G), Dense ↑S ∨ ∃ a, S = Subgroup.closure {a}
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.instReprEMatchTheoremConstraint : Repr Lean.Meta.Grind.EMatchTheoremConstraint
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.vadd_const : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [inst : TopologicalSpace β] {𝕜 : Type u_5}
  [inst_1 : TopologicalSpace 𝕜] [inst_2 : VAdd 𝕜 β] [ContinuousVAdd 𝕜 β] {f : α → 𝕜},
  MeasureTheory.StronglyMeasurable f → ∀ (c : β), MeasureTheory.StronglyMeasurable fun x => f x +ᵥ c
-- Std.Sat.AIG.RelabelNat
/-- Insert a `Decl.false` into the `State` structure.
 -/
Std.Sat.AIG.RelabelNat.State.addFalse : {α : Type} →
  [inst : DecidableEq α] →
    [inst_1 : Hashable α] →
      {idx : ℕ} →
        {decls : Array (Std.Sat.AIG.Decl α)} →
          {hidx : idx < decls.size} →
            Std.Sat.AIG.RelabelNat.State α decls idx →
              decls[idx] = Std.Sat.AIG.Decl.false → Std.Sat.AIG.RelabelNat.State α decls (idx + 1)
-- Mathlib.Algebra.Homology.ComplexShape
ComplexShape.refl_Rel : ∀ (ι : Type u_2) (i j : ι), (ComplexShape.refl ι).Rel i j = (i = j)
-- Lean.Server.References
/-- Global reference. Used by the language server to figure out which identifiers refer to which
other identifiers across the whole project.
 -/
Lean.Server.Reference : Type
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddModObj.add_vadd_self : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (M : C)
  [inst_2 : CategoryTheory.AddMonObj M] (X : C) [inst_3 : CategoryTheory.AddModObj M X],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.AddMonObj.add X)
      CategoryTheory.AddModObj.vadd =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M M X).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M CategoryTheory.AddModObj.vadd)
        CategoryTheory.AddModObj.vadd)
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommGroupWithTop.sub_self_nonneg : ∀ {α : Type u_2} [inst : LinearOrderedAddCommGroupWithTop α] {a : α}, 0 ≤ a - a
-- Mathlib.Analysis.Normed.Affine.AddTorsor
dist_midpoint_midpoint_le : ∀ {V : Type u_1} [inst : SeminormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] (p₁ p₂ p₃ p₄ : V),
  dist (midpoint ℝ p₁ p₂) (midpoint ℝ p₃ p₄) ≤ (dist p₁ p₃ + dist p₂ p₄) / 2
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.nfp_mul_one : ∀ {a : Ordinal.{u_1}}, 0 < a → Ordinal.nfp (fun x => a * x) 1 = a ^ Ordinal.omega0
-- Mathlib.Algebra.Homology.BifunctorFlip
HomologicalComplex.mapBifunctorFlipIso_hom_naturality : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D] {I₁ : Type u_4}
  {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Preadditive D] {K₁ L₁ : HomologicalComplex C₁ c₁} (φ₁ : K₁ ⟶ L₁)
  {K₂ L₂ : HomologicalComplex C₂ c₂} (φ₂ : K₂ ⟶ L₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
  [inst_6 : F.PreservesZeroMorphisms] [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J)
  [inst_8 : TotalComplexShape c₁ c₂ c] [inst_9 : TotalComplexShape c₂ c₁ c]
  [inst_10 : TotalComplexShapeSymmetry c₁ c₂ c] [inst_11 : DecidableEq J] [inst_12 : K₁.HasMapBifunctor K₂ F c]
  [inst_13 : L₁.HasMapBifunctor L₂ F c],
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctorMap φ₂ φ₁ F.flip c)
      (L₁.mapBifunctorFlipIso L₂ F c).hom =
    CategoryTheory.CategoryStruct.comp (K₁.mapBifunctorFlipIso K₂ F c).hom
      (HomologicalComplex.mapBifunctorMap φ₁ φ₂ F c)
-- Init.Data.Order.Opposite
Std.OppositeOrderInstances.instLEAsymmOpposite : ∀ {α : Type u_1} {i : LE α} [Std.Asymm fun x1 x2 => x1 ≤ x2], Std.Asymm fun x1 x2 => x1 ≤ x2
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Substructure
Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go_lt_size_of_lt_aig_size : ∀ {x : ℕ} (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (expr : Std.Tactic.BVDecide.BVLogicalExpr)
  (cache : Std.Tactic.BVDecide.BVExpr.Cache aig),
  x < aig.decls.size → x < (↑(Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go aig expr cache).result).aig.decls.size
-- Mathlib.Analysis.Normed.Module.Bases
/-- The action of the projection on a vector `x`.  -/
GeneralSchauderBasis.proj_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {X : Type u_2} [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] {β : Type u_3} {L : SummationFilter β} (b : GeneralSchauderBasis β 𝕜 X L) (A : Finset β)
  (x : X), (b.proj A) x = ∑ i ∈ A, (b.coord i) x • ↑b i
-- Mathlib.NumberTheory.FLT.Three
/-- Given `S : Solution`, we construct `S₁ : Solution'`, with smaller multiplicity of `λ` in
`c` (see `Solution'_descent_multiplicity_lt` below.).  -/
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.Solution'_descent : {K : Type u_1} →
  [inst : Field K] →
    {ζ : K} →
      {hζ : IsPrimitiveRoot ζ 3} →
        FermatLastTheoremForThreeGen.Solution✝ hζ →
          [inst_1 : NumberField K] → [IsCyclotomicExtension {3} ℚ K] → FermatLastTheoremForThreeGen.Solution'✝ hζ
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.tactic.simp.user.exampleNat : Lean.Option ℕ
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.isoCycles₁_hom_comp_i : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.CategoryStruct.comp (groupHomology.isoCycles₁ A).hom
      (groupHomology.shortComplexH1 A).moduleCatLeftHomologyData.i =
    CategoryTheory.CategoryStruct.comp (groupHomology.iCycles A 1) (groupHomology.chainsIso₁ A).hom
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.equivComma_inverse_obj_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (c : CategoryTheory.Comma (CategoryTheory.Functor.const C) (CategoryTheory.Functor.id (CategoryTheory.Functor C D)))
  (X : CategoryTheory.WithInitial C),
  (CategoryTheory.WithInitial.equivComma.inverse.obj c).obj X =
    match X with
    | CategoryTheory.WithInitial.of x => c.right.obj x
    | CategoryTheory.WithInitial.star => c.left
-- Std.Data.HashSet.Lemmas
Std.HashSet.contains_toArray : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α},
  m.toArray.contains k = m.contains k
-- Mathlib.Data.Finset.Image
Finset.equivMap_apply_coe : ∀ {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : Finset α) (x : ↥s), ↑((Finset.equivMap f s) x) = f ↑x
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.applyPartition.go.match_1.eq_3 : ∀ (motive : Ordering → Sort u_1) (h_1 : Ordering.gt = Ordering.lt → motive Ordering.lt)
  (h_2 : Ordering.gt = Ordering.eq → motive Ordering.eq) (h_3 : Ordering.gt = Ordering.gt → motive Ordering.gt),
  (match h : Ordering.gt with
    | Ordering.lt => h_1 h
    | Ordering.eq => h_2 h
    | Ordering.gt => h_3 h) =
    h_3 ⋯
-- Mathlib.NumberTheory.NumberField.Basic
Rat.ringOfIntegersEquiv_apply_coe : ∀ (z : NumberField.RingOfIntegers ℚ), ↑(Rat.ringOfIntegersEquiv z) = (algebraMap (NumberField.RingOfIntegers ℚ) ℚ) z
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
/-- For disjoint `f1` and `f2`, and function `g`, the product of the products of `g`
over `f1` and `f2` equals the product of `g` over `f1 + f2`  -/
Finsupp.prod_add_index_of_disjoint : ∀ {α : Type u_1} {M : Type u_8} [inst : AddCommMonoid M] {f1 f2 : α →₀ M},
  Disjoint f1.support f2.support →
    ∀ {β : Type u_16} [inst_1 : CommMonoid β] (g : α → M → β), (f1 + f2).prod g = f1.prod g * f2.prod g
-- Mathlib.MeasureTheory.Measure.Prod
/-- If `Prod.fst ⁻¹' s` is a null measurable set and `ν ≠ 0`, then `s` is a null measurable set.  -/
MeasureTheory.NullMeasurableSet.of_preimage_fst : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [NeZero ν] {s : Set α},
  MeasureTheory.NullMeasurableSet (Prod.fst ⁻¹' s) (μ.prod ν) → MeasureTheory.NullMeasurableSet s μ
-- Mathlib.Dynamics.TopologicalEntropy.Semiconj
/-- The entropy of the restriction of `T` to an invariant set `F` is `coverEntropy T F`. This
theorem justifies our definition of `coverEntropy T F`.  -/
Dynamics.coverEntropy_restrict : ∀ {X : Type u_1} [inst : UniformSpace X] {T : X → X} {F : Set X} (h : Set.MapsTo T F F),
  Dynamics.coverEntropy (Set.MapsTo.restrict T F F h) Set.univ = Dynamics.coverEntropy T F
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem?_modify_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {f : β → β}, (m.modify k f)[k]? = Option.map f m[k]?
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
/-- Every property local at the target can be associated with an affine target property.
This is not an instance as the associated property can often take on simpler forms.  -/
AlgebraicGeometry.HasAffineProperty.of_isZariskiLocalAtTarget : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsZariskiLocalAtTarget P],
  AlgebraicGeometry.HasAffineProperty P (AlgebraicGeometry.AffineTargetMorphismProperty.of P)
-- Mathlib.GroupTheory.Nilpotent
Subgroup.upperCentralSeriesStep.congr_simp : ∀ {G : Type u_1} [inst : Group G] (N N_1 : Subgroup G) (e_N : N = N_1) [inst_1 : N.Normal],
  N.upperCentralSeriesStep = N_1.upperCentralSeriesStep
-- Mathlib.GroupTheory.Complement
AddSubgroup.IsComplement.toLeftFun.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {S : Set G} (hS : AddSubgroup.IsComplement S ↑H),
  hS.toLeftFun = ⇑hS.leftQuotientEquiv ∘ Quotient.mk''
-- Mathlib.Topology.UniformSpace.Defs
UniformSpace.mem_nhds_iff_symm : ∀ {α : Type ua} [inst : UniformSpace α] {x : α} {s : Set α},
  s ∈ nhds x ↔ ∃ V ∈ uniformity α, SetRel.IsSymm V ∧ UniformSpace.ball x V ⊆ s
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_const_one : ∀ (R : Type u_1) {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (a : A),
  autoParam (p a) _auto_255✝ → cfc (fun x => 1) a = 1
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.containsKey.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a : α) (x : List ((a : α) × β a)),
  Std.Internal.List.containsKey a x =
    match x with
    | [] => false
    | ⟨k, snd⟩ :: l => k == a || Std.Internal.List.containsKey a l
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.eq_re_iff_mem_range_coe : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : CommRing R] {a : QuaternionAlgebra R c₁ c₂ c₃},
  a = ↑a.re ↔ a ∈ Set.range QuaternionAlgebra.coe
-- Std.Data.HashSet.Lemmas
Std.HashSet.mem_iff_contains : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} {a : α}, a ∈ m ↔ m.contains a = true
-- Mathlib.NumberTheory.ModularForms.Discriminant
/-- The discriminant satisfies the modular transformation for `S : z ↦ -1 / z`:
we have `Δ(-1 / z) = z ^ 12 · Δ(z)`.  -/
ModularForm.discriminant_S_invariant : SlashAction.map 12 ModularGroup.S ModularForm.discriminant = ModularForm.discriminant
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.limitBiconeOfUnique_isBilimit_isLimit : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_2 : Unique J] (f : J → C),
  (CategoryTheory.Limits.limitBiconeOfUnique f).isBilimit.isLimit = (CategoryTheory.Limits.limitConeOfUnique f).isLimit
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.Hom.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {M N : CategoryTheory.Mon C} {hom : M.X ⟶ N.X} {isMonHom_hom : CategoryTheory.IsMonHom hom} {hom_1 : M.X ⟶ N.X}
  {isMonHom_hom_1 : CategoryTheory.IsMonHom hom_1},
  { hom := hom, isMonHom_hom := isMonHom_hom } = { hom := hom_1, isMonHom_hom := isMonHom_hom_1 } → hom = hom_1
-- Mathlib.Analysis.Calculus.FDeriv.Add
fderivWithin_add : ∀ {𝕜 : 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 g : E → F}
  {x : E} {s : Set E},
  UniqueDiffWithinAt 𝕜 s x →
    DifferentiableWithinAt 𝕜 f s x →
      DifferentiableWithinAt 𝕜 g s x → fderivWithin 𝕜 (f + g) s x = fderivWithin 𝕜 f s x + fderivWithin 𝕜 g s x
-- Std.Data.Iterators.Lemmas.Combinators.DropWhile
Std.Iter.step_dropWhile : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {P : β → Bool} {it : Std.Iter β},
  (Std.Iter.dropWhile P it).step =
    match it.step with
    | ⟨Std.IterStep.yield it' out, h⟩ =>
      match hP : P out with
      | true => Std.PlausibleIterStep.skip (Std.Iter.Intermediate.dropWhile P true it') ⋯
      | false => Std.PlausibleIterStep.yield (Std.Iter.Intermediate.dropWhile P false it') out ⋯
    | ⟨Std.IterStep.skip it', h⟩ => Std.PlausibleIterStep.skip (Std.Iter.Intermediate.dropWhile P true it') ⋯
    | ⟨Std.IterStep.done, h⟩ => Std.PlausibleIterStep.done ⋯
-- Init.Data.List.Lemmas
List.foldl_ite_right : ∀ {α : Type u_1} {β : Type u_2} {P : α → Prop} [inst : DecidablePred P] {l : List α} {f : β → α → β} {init : β},
  List.foldl (fun sofar a => if P a then sofar else f sofar a) init l =
    List.foldl f init (List.filter (fun a => decide ¬P a) l)
-- Init.Data.Iterators.Lemmas.Consumers.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Loop.0.Std.Iter.findSomeM?.match_1.eq_1 : ∀ {γ : Type u_1} (motive : Option γ → Sort u_2) (h_1 : Unit → motive none) (h_2 : (fx : γ) → motive (some fx)),
  (match none with
    | none => h_1 ()
    | some fx => h_2 fx) =
    h_1 ()
-- Mathlib.RingTheory.LocalRing.RingHom.Basic
/-- Every ring hom `f : K →+* R` from a division ring `K` to a nontrivial ring `R` is a
local ring hom.  -/
IsLocalRing.instIsLocalHomRingHomOfNontrivial : ∀ {K : Type u_4} {R : Type u_5} [inst : DivisionRing K] [inst_1 : CommRing R] [Nontrivial R] (f : K →+* R), IsLocalHom f
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.mem_ground_of_mem_closure : ∀ {α : Type u_2} {M : Matroid α} {X : Set α} {e : α}, e ∈ M.closure X → e ∈ M.E
-- Mathlib.Data.Seq.Computation
Computation.rmap.eq_2 : ∀ {α : Type u} {β : Type v} {γ : Type w} (f : β → γ) (val : β), Computation.rmap f (Sum.inr val) = Sum.inr (f val)
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.comap_map_comap : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] {S : AddSubmonoid N} {f : F},
  AddSubmonoid.comap f (AddSubmonoid.map f (AddSubmonoid.comap f S)) = AddSubmonoid.comap f S
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.IterM.step_filterMapWithPostcondition.match_3.eq_2 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (it' : Std.IterM m β) (h : it.IsPlausibleStep (Std.IterStep.skip it'))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.skip it', h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_2 it' h
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.AppMatchState.mk : Lean.Meta.MatcherInfo →
  Lean.SubExpr →
    Option (Lean.Term × Lean.Expr) →
      Bool →
        Array Lean.Term →
          Array (Option Lean.Name) →
            Array Lean.SubExpr →
              Array (Array Lean.Name) → Array Lean.Term → Lean.PrettyPrinter.Delaborator.AppMatchState
-- Mathlib.NumberTheory.Transcendental.Liouville.Measure
/-- The filters `residual ℝ` and `ae volume` are disjoint. This means that there exists a residual
set of Lebesgue measure zero (e.g., the set of Liouville numbers).  -/
Real.disjoint_residual_ae : Disjoint (residual ℝ) (MeasureTheory.ae MeasureTheory.volume)
-- Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
/-- Left homotopic edges represent the same morphism in the homotopy category.
 -/
SSet.Truncated.HomotopicL.congr_homotopyCategory₂HomMk : ∀ {A : SSet.Truncated 2} [inst : A.Quasicategory₂]
  {x y : A.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Quasicategory₂._proof_1 })}
  {f g : SSet.Truncated.Edge x y},
  SSet.Truncated.HomotopicL f g → SSet.Truncated.HomotopyCategory₂.homMk f = SSet.Truncated.HomotopyCategory₂.homMk g
-- Mathlib.Data.Sign.Defs
_private.Mathlib.Data.Sign.Defs.0.SignType.fin3Equiv.match_1.eq_3 : ∀ (motive : SignType → Sort u_1) (h_1 : Unit → motive SignType.zero) (h_2 : Unit → motive SignType.pos)
  (h_3 : Unit → motive SignType.neg),
  (match SignType.neg with
    | SignType.zero => h_1 ()
    | SignType.pos => h_2 ()
    | SignType.neg => h_3 ()) =
    h_3 ()