mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Euclidean.Volume.Measure
MeasureTheory.Measure.euclideanHausdorffMeasure_smul₀ : ∀ {𝕜 : Type u_3} {E : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedDivisionRing 𝕜] [inst_2 : Module 𝕜 E]
  [NormSMulClass 𝕜 E] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E] (d : ℕ) {r : 𝕜},
  r ≠ 0 →
    ∀ (s : Set E),
      (MeasureTheory.Measure.euclideanHausdorffMeasure d) (r • s) =
        ‖r‖₊ ^ d • (MeasureTheory.Measure.euclideanHausdorffMeasure d) s
-- Mathlib.Analysis.SpecificLimits.Basic
NNRat.tendsto_algebraMap_inv_atTop_nhds_zero_nat : ∀ (𝕜 : Type u_4) [inst : Semiring 𝕜] [inst_1 : Algebra ℚ≥0 𝕜] [inst_2 : TopologicalSpace 𝕜] [ContinuousSMul ℚ≥0 𝕜],
  Filter.Tendsto (⇑(algebraMap ℚ≥0 𝕜) ∘ fun n => (↑n)⁻¹) Filter.atTop (nhds 0)
-- Mathlib.Logic.Embedding.Basic
/-- Choosing an element `b : β` gives an embedding of `PUnit` into `β`.  -/
Function.Embedding.punit : {β : Sort u_1} → β → PUnit.{u_2} ↪ β
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.prod.congr_simp : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} {inst : DecidableEq ι} [inst_1 : DecidableEq ι]
  [inst_2 : (i : ι) → Zero (β i)] {inst_3 : (i : ι) → (x : β i) → Decidable (x ≠ 0)}
  [inst_4 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_5 : CommMonoid γ] (f f_1 : Π₀ (i : ι), β i),
  f = f_1 → ∀ (g g_1 : (i : ι) → β i → γ), g = g_1 → f.prod g = f_1.prod g_1
-- Init.Data.Array.Lemmas
Array.map_singleton : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {a : α}, Array.map f #[a] = #[f a]
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
/-- If an alternating map `f` satisfies a boundedness property around `0`,
one can deduce a bound on `f m₁ - f m₂` using the multilinearity.
Here, we give a precise but hard to use version.
See `AlternatingMap.norm_image_sub_le_of_bound` for a less precise but more usable version.
The bound reads
`‖f m - f m'‖ ≤
  C * ‖m 1 - m' 1‖ * max ‖m 2‖ ‖m' 2‖ * max ‖m 3‖ ‖m' 3‖ * ... * max ‖m n‖ ‖m' n‖ + ...`,
where the other terms in the sum are the same products where `1` is replaced by any `i`.  -/
AlternatingMap.norm_image_sub_le_of_bound' : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : Fintype ι] [inst_6 : DecidableEq ι] (f : E [⋀^ι]→ₗ[𝕜] F) {C : ℝ},
  0 ≤ C →
    (∀ (m : ι → E), ‖f m‖ ≤ C * ∏ i, ‖m i‖) →
      ∀ (m₁ m₂ : ι → E), ‖f m₁ - f m₂‖ ≤ C * ∑ i, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
-- Lean.Elab.ParseImportsFast
Lean.ParseImports.finishCommentBlock : ℕ → Lean.ParseImports.Parser
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isBigO_const_smul_left : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} {𝕜 : Type u_15} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E']
  [inst_2 : NormedDivisionRing 𝕜] {g : α → F} {f' : α → E'} {l : Filter α} [inst_3 : Module 𝕜 E'] [NormSMulClass 𝕜 E']
  {c : 𝕜}, c ≠ 0 → ((fun x => c • f' x) =O[l] g ↔ f' =O[l] g)
-- Mathlib.CategoryTheory.Types.Basic
CategoryTheory.eqToHom_map_comp_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y Z : C} (p : X = Y) (q : Y = Z) {F_1 : D → D → Type uF} {carrier : D → Type w}
  {instFunLike : (X Y : D) → FunLike (F_1 X Y) (carrier X) (carrier Y)} [inst_2 : CategoryTheory.ConcreteCategory D F_1]
  (x : carrier (F.obj X)),
  (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.eqToHom q)))
      ((CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.eqToHom p))) x) =
    (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.eqToHom ⋯))) x
-- Mathlib.Tactic.CategoryTheory.Coherence.PureCoherence
/-- Meta version of `CategoryTheory.FreeBicategory.normalize_naturality`.  -/
Mathlib.Tactic.BicategoryLike.naturality : {ρ : Type} →
  [Mathlib.Tactic.BicategoryLike.MonadMor₁ (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
    [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
      [Mathlib.Tactic.BicategoryLike.MonadCoherehnceHom (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
        [Mathlib.Tactic.BicategoryLike.MonadNormalizeNaturality (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
          Lean.Name →
            Mathlib.Tactic.BicategoryLike.NormalizedHom →
              Mathlib.Tactic.BicategoryLike.Mor₂Iso → Mathlib.Tactic.BicategoryLike.CoherenceM ρ Lean.Expr
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.Cell.ι_t_app : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] {f : P.RankFunction ι}
  [inst_1 : P.IsProper] {j : ι} (c : f.Cell j) (x : SimplexCategoryᵒᵖ),
  CategoryTheory.CategoryStruct.comp (c.ιSigmaHorn.app x) ((f.t j).app x) =
    (SSet.Subcomplex.Pairing.RankFunction.Cell.mapHorn f c).app x
-- Mathlib.SetTheory.Cardinal.NatCard
Finite.card_range_le : ∀ {α : Type u_1} {β : Type u_2} [Finite α] (f : α → β), Nat.card ↑(Set.range f) ≤ Nat.card α
-- Mathlib.Analysis.Normed.Module.DoubleDual
NormedSpace.double_dual_bound : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] (E : Type u_2) [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (x : E), ‖(NormedSpace.inclusionInDoubleDual 𝕜 E) x‖ ≤ ‖x‖
-- Std.Http.Data.URI.Basic
/-- Optional fragment identifier (the part after '#'), percent-encoded.
 -/
Std.Http.URI.fragment : Std.Http.URI → Option String
-- Mathlib.Data.Fintype.OfMap
/-- If `f : α → β` is a surjection and `α` is a fintype, then `β` is also a fintype.  -/
Fintype.ofSurjective : {α : Type u_1} → {β : Type u_2} → [DecidableEq β] → [Fintype α] → (f : α → β) → Function.Surjective f → Fintype β
-- Mathlib.Combinatorics.Quiver.Basic
Quiver.heq_of_homOfEq_ext : ∀ {V : Type u_1} [inst : Quiver V] {X Y X' Y' : V} (hX : X = X') (hY : Y = Y') {f : X ⟶ Y} {f' : X' ⟶ Y'},
  Quiver.homOfEq f hX hY = f' → f ≍ f'
-- Mathlib.Algebra.Quaternion
Quaternion.imK_smul : ∀ {S : Type u_1} {R : Type u_3} [inst : CommRing R] (a : Quaternion R) [inst_1 : SMul S R] (s : S),
  (s • a).imK = s • a.imK
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingHom.instInhabited : (α : Type u_2) → [inst : NonAssocSemiring α] → [inst_1 : Preorder α] → Inhabited (α →+*o α)
-- Mathlib.RingTheory.Derivation.Lie
Derivation.Compatible.mk_left : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra R A] {A' : Type u_3}
  [inst_3 : CommRing A'] [inst_4 : Algebra R A'] [inst_5 : Algebra A A'] [inst_6 : IsScalarTower R A A']
  (x : Derivation R A' A') (y : Derivation R A A) (h : ⇑x ∘ ⇑(Algebra.ofId A A') = ⇑(Algebra.ofId A A') ∘ ⇑y),
  (↑(Derivation.Compatible.mk x y h)).1 = x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
CategoryTheory.Limits.pullbackSymmetry_hom_of_mono_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.Mono f],
  (CategoryTheory.Limits.pullbackSymmetry f f).hom =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback f f)
-- Mathlib.Algebra.Module.Submodule.Map
/-- Given modules `M`, `M₂` over a commutative ring, together with submodules `p ⊆ M`, `q ⊆ M₂`,
the set of maps $\{f ∈ Hom(M, M₂) | f(p) ⊆ q \}$ is a submodule of `Hom(M, M₂)`.  -/
Submodule.compatibleMaps : {S : Type u_9} →
  {N : Type u_10} →
    {N₂ : Type u_11} →
      [inst : CommSemiring S] →
        [inst_1 : AddCommMonoid N] →
          [inst_2 : AddCommMonoid N₂] →
            [inst_3 : Module S N] → [inst_4 : Module S N₂] → Submodule S N → Submodule S N₂ → Submodule S (N →ₗ[S] N₂)
-- Mathlib.MeasureTheory.Measure.TightNormed
MeasureTheory.tendsto_measure_norm_gt_of_isTightMeasureSet : ∀ {E : Type u_1} {mE : MeasurableSpace E} {S : Set (MeasureTheory.Measure E)} [inst : NormedAddCommGroup E],
  MeasureTheory.IsTightMeasureSet S → Filter.Tendsto (fun r => ⨆ μ ∈ S, μ {x | r < ‖x‖}) Filter.atTop (nhds 0)
-- Mathlib.Algebra.GCDMonoid.Multiset
Multiset.gcd_eq_zero_iff : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (s : Multiset α),
  s.gcd = 0 ↔ ∀ x ∈ s, x = 0
-- Mathlib.Probability.Kernel.Composition.Comp
ProbabilityTheory.Kernel.comp_add_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (μ : ProbabilityTheory.Kernel α β) (κ η : ProbabilityTheory.Kernel β γ),
  (κ + η).comp μ = κ.comp μ + η.comp μ
-- Mathlib.Analysis.SpecificLimits.Normed
summable_descFactorial_mul_geometric_of_norm_lt_one : ∀ {R : Type u_4} [inst : NormedRing R] [HasSummableGeomSeries R] (k : ℕ) {r : R},
  ‖r‖ < 1 → Summable fun n => ↑((n + k).descFactorial k) * r ^ n
-- Batteries.Data.Vector.Lemmas
Vector.get_eq_getElem : ∀ {α : Type u_1} {n : ℕ} (v : Vector α n) (i : Fin n), v.get i = v[↑i]
-- Mathlib.Topology.Instances.NNReal.Lemmas
NNReal.iSup_pow_of_ne_zero : ∀ {ι : Sort u_1} {n : ℕ}, n ≠ 0 → ∀ (f : ι → NNReal), (⨆ i, f i) ^ n = ⨆ i, f i ^ n
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.C_two : ∀ (R : Type u_1) [inst : CommRing R], Polynomial.Chebyshev.C R 2 = Polynomial.X ^ 2 - 2
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
/-- A global presentation of a sheaf of module if finite if the type
of generators and relations are finite.  -/
SheafOfModules.Presentation.IsFinite : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat] →
          [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] → {M : SheafOfModules R} → M.Presentation → Prop
-- Std.Tactic.BVDecide.LRAT.Actions
Std.Tactic.BVDecide.LRAT.Action.del.inj : ∀ {β : Type u} {α : Type v} {ids ids_1 : Array ℕ},
  Std.Tactic.BVDecide.LRAT.Action.del ids = Std.Tactic.BVDecide.LRAT.Action.del ids_1 → ids = ids_1
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.SimpleFunc.integral_sub : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : NormedSpace ℝ E] {f g : MeasureTheory.SimpleFunc α E},
  MeasureTheory.Integrable (⇑f) μ →
    MeasureTheory.Integrable (⇑g) μ →
      MeasureTheory.SimpleFunc.integral μ (f - g) =
        MeasureTheory.SimpleFunc.integral μ f - MeasureTheory.SimpleFunc.integral μ g
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.join_congr : ∀ {α : Type u} {S T : Stream'.WSeq (Stream'.WSeq α)}, Stream'.WSeq.LiftRel Stream'.WSeq.Equiv S T → S.join ~ʷ T.join
-- Mathlib.AlgebraicTopology.SimplicialSet.Dimension
SSet.nonDegenerate_eq_empty_of_hasDimensionLT : ∀ (X : SSet) (d : ℕ) [X.HasDimensionLT d] (n : ℕ),
  autoParam (d ≤ n) SSet.nonDegenerate_eq_empty_of_hasDimensionLT._auto_1 → X.nonDegenerate n = ∅
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.cast_apply : ∀ {ι : Type u_7} {R : ι → Type u_8} [inst : (i : ι) → Mul (R i)] [inst_1 : (i : ι) → Add (R i)] {i j : ι} (h : i = j)
  (a : R i), (RingEquiv.cast h) a = cast ⋯ a
-- Mathlib.Logic.Encodable.Basic
/-- Lifts an `a : ULower α` into `α`.  -/
ULower.up : {α : Type u_1} → [inst : Encodable α] → ULower α → α
-- Mathlib.SetTheory.Ordinal.Exponential
/-- `opow b` and `log b` (almost) form a Galois connection.

See `lt_opow_iff_log_lt'` for a variant assuming `c ≠ 0` rather than `x ≠ 0`. See also
`lt_opow_of_log_lt` and `lt_log_of_lt_opow`, which are both separate implications under weaker
assumptions.  -/
Ordinal.lt_opow_iff_log_lt : ∀ {b x c : Ordinal.{u_1}}, 1 < b → x ≠ 0 → (x < b ^ c ↔ Ordinal.log b x < c)
-- Mathlib.Algebra.Polynomial.Smeval
Polynomial.eval₂_smulOneHom_eq_smeval : ∀ (R : Type u_3) [inst : Semiring R] {S : Type u_4} [inst_1 : Semiring S] [inst_2 : Module R S]
  [inst_3 : IsScalarTower R S S] (p : Polynomial R) (x : S), Polynomial.eval₂ RingHom.smulOneHom x p = p.smeval x
-- Init.Data.SInt.Lemmas
Int64.toISize_ofIntLE : ∀ {n : ℤ} (h₁ : Int64.minValue.toInt ≤ n) (h₂ : n ≤ Int64.maxValue.toInt),
  (Int64.ofIntLE n h₁ h₂).toISize = ISize.ofInt n
-- Mathlib.Data.Finset.SMulAntidiagonal
Finset.mem_smulAntidiagonal : ∀ {G : Type u_1} {P : Type u_2} [inst : SMul G P] {s : Set G} {t : Set P} (a : P) (h : (s.smulAntidiagonal t a).Finite)
  {x : G × P}, x ∈ Finset.SMulAntidiagonal a h ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 • x.2 = a
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.map_comp : ∀ {R : Type u_1} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_5} {M₂ : Type u_7} {M₃ : Type u_8} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] [inst_6 : Module R M] [inst_7 : Module R₂ M₂] [inst_8 : Module R₃ M₃] {σ₁₂ : R →+* R₂}
  {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_10 : RingHomSurjective σ₁₂]
  [inst_11 : RingHomSurjective σ₂₃] [inst_12 : RingHomSurjective σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] M₃)
  (p : Submodule R M), Submodule.map (g ∘ₛₗ f) p = Submodule.map g (Submodule.map f p)
-- Init.Data.Float.Float
instAddFloat : Add Float
-- Init.Data.SInt.Bitwise
instLawfulCommIdentityInt8HXorOfNat : Std.LawfulCommIdentity (fun x1 x2 => x1 ^^^ x2) 0
-- Std.Http.Data.Response
/-- Adds a single header to the response being built, panics if the header is invalid.
 -/
Std.Http.Response.Builder.header! : Std.Http.Response.Builder → String → String → Std.Http.Response.Builder
-- Mathlib.Combinatorics.SimpleGraph.Sum
SimpleGraph.not_preconnected_sum : ∀ {V : Type u_3} {W : Type u_5} {G : SimpleGraph V} {H : SimpleGraph W} [Nonempty V] [Nonempty W],
  ¬(G ⊕g H).Preconnected
-- Mathlib.FieldTheory.Separable
Polynomial.exists_finset_of_splits : ∀ {F : Type u} [inst : Field F] {K : Type v} [inst_1 : Field K] (i : F →+* K) {f : Polynomial F},
  f.Separable →
    (Polynomial.map i f).Splits →
      ∃ s, Polynomial.map i f = Polynomial.C (i f.leadingCoeff) * ∏ a ∈ s, (Polynomial.X - Polynomial.C a)
-- Mathlib.Algebra.Homology.ComplexShape
ComplexShape.mk.injEq : ∀ {ι : Type u_1} (Rel : ι → ι → Prop) (next_eq : ∀ {i j j' : ι}, Rel i j → Rel i j' → j = j')
  (prev_eq : ∀ {i i' j : ι}, Rel i j → Rel i' j → i = i') (Rel_1 : ι → ι → Prop)
  (next_eq_1 : ∀ {i j j' : ι}, Rel_1 i j → Rel_1 i j' → j = j')
  (prev_eq_1 : ∀ {i i' j : ι}, Rel_1 i j → Rel_1 i' j → i = i'),
  ({ Rel := Rel, next_eq := next_eq, prev_eq := prev_eq } =
      { Rel := Rel_1, next_eq := next_eq_1, prev_eq := prev_eq_1 }) =
    (Rel = Rel_1)
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.commRing : {R : Type u} →
  {M : Type v} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → [inst_3 : Module Rᵐᵒᵖ M] → [IsCentralScalar R M] → CommRing (TrivSqZeroExt R M)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Countable
MeasureTheory.univ_le_of_forall_fin_meas_le : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0)
  [MeasureTheory.SigmaFinite (μ.trim hm)] (C : ENNReal) {f : Set α → ENNReal},
  (∀ (s : Set α), MeasurableSet s → μ s ≠ ⊤ → f s ≤ C) →
    (∀ (S : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (S n)) → Monotone S → f (⋃ n, S n) ≤ ⨆ n, f (S n)) → f Set.univ ≤ C
-- Init.Data.UInt.Bitwise
Bool.toBitVec_toUSize : ∀ {b : Bool}, b.toUSize.toBitVec = BitVec.setWidth System.Platform.numBits (BitVec.ofBool b)
-- Mathlib.Analysis.Complex.Trigonometric
Complex.cos_two_mul : ∀ (x : ℂ), Complex.cos (2 * x) = 2 * Complex.cos x ^ 2 - 1
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
SlashInvariantForm.instIsSubApplyUpperHalfPlaneComplex : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ}, IsSubApply (SlashInvariantForm Γ k) UpperHalfPlane ℂ
-- Mathlib.Data.Complex.Basic
Complex.normSq_one : Complex.normSq 1 = 1
-- Init.Grind.Config
Lean.Grind.instBEqConfig : BEq Lean.Grind.Config
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.IsStrictRestriction.eq_restrict : ∀ {α : Type u_1} {M N : Matroid α}, N.IsStrictRestriction M → M.restrict N.E = N
-- Mathlib.Algebra.Quaternion
/-- The imaginary part of a quaternion.  -/
Quaternion.im : {R : Type u_3} → [inst : CommRing R] → Quaternion R → Quaternion R
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsAtomic.equal : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} (t₁ t₂ : L.Term (α ⊕ Fin n)), (t₁.bdEqual t₂).IsAtomic
-- Mathlib.Algebra.BigOperators.Group.Finset.Indicator
Finset.indicator_biUnion : ∀ {ι : Type u_1} {κ : Type u_2} {β : Type u_4} [inst : AddCommMonoid β] (s : Finset ι) (t : ι → Set κ) {f : κ → β},
  (↑s).PairwiseDisjoint t → (⋃ i ∈ s, t i).indicator f = fun a => ∑ i ∈ s, (t i).indicator f a
-- Lean.Expr
Lean.Nat.mkInstNatPow : Lean.Expr
-- Mathlib.Algebra.Order.Group.Indicator
Set.indicator_nonpos_le_indicator : ∀ {α : Type u_2} {M : Type u_3} [inst : Zero M] [inst_1 : LinearOrder M] (s : Set α) (f : α → M),
  {a | f a ≤ 0}.indicator f ≤ s.indicator f
-- Mathlib.Algebra.Ring.Ext
CommSemiring.toSemiring_injective : ∀ {R : Type u}, Function.Injective (@CommSemiring.toSemiring R)
-- Mathlib.Topology.Connected.Basic
IsPreirreducible.isPreconnected : ∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α}, IsPreirreducible s → IsPreconnected s
-- Mathlib.Algebra.GroupWithZero.Basic
sq_eq_zero_iff : ∀ {M₀ : Type u_1} [inst : MonoidWithZero M₀] {a : M₀} [IsReduced M₀], a ^ 2 = 0 ↔ a = 0
-- Init.Data.Nat.Lemmas
Nat.div_dvd_iff_dvd_mul : ∀ {a b c : ℕ}, b ∣ a → 0 < b → (a / b ∣ c ↔ a ∣ b * c)
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.WalkingParallelFamily.Hom.line.inj : ∀ {J : Type w} {a a_1 : J},
  CategoryTheory.Limits.WalkingParallelFamily.Hom.line a = CategoryTheory.Limits.WalkingParallelFamily.Hom.line a_1 →
    a = a_1
-- Mathlib.Algebra.CharP.Lemmas
sub_pow_expChar_pow : ∀ {R : Type u_1} [inst : CommRing R] (x y : R) (n : ℕ) {p : ℕ} [hR : ExpChar R p],
  (x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n
-- Init.Grind.AC
Lean.Grind.AC.Seq.eraseDup.induct_unfolding : ∀ (motive : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Prop),
  (∀ (x : Lean.Grind.AC.Var), motive (Lean.Grind.AC.Seq.var x) (Lean.Grind.AC.Seq.var x)) →
    (∀ (x : Lean.Grind.AC.Var) (s : Lean.Grind.AC.Seq),
        have s' := s.eraseDup;
        ∀ (x_1 : Lean.Grind.AC.Var),
          s' = Lean.Grind.AC.Seq.var x_1 →
            Nat.beq x x_1 = true →
              motive s s.eraseDup → motive (Lean.Grind.AC.Seq.cons x s) (Lean.Grind.AC.Seq.var x)) →
      (∀ (x : Lean.Grind.AC.Var) (s : Lean.Grind.AC.Seq),
          have s' := s.eraseDup;
          ∀ (x_1 : Lean.Grind.AC.Var),
            s' = Lean.Grind.AC.Seq.var x_1 →
              ¬Nat.beq x x_1 = true →
                motive s s.eraseDup →
                  motive (Lean.Grind.AC.Seq.cons x s) (Lean.Grind.AC.Seq.cons x (Lean.Grind.AC.Seq.var x_1))) →
        (∀ (x : Lean.Grind.AC.Var) (s : Lean.Grind.AC.Seq),
            have s' := s.eraseDup;
            ∀ (x_1 : Lean.Grind.AC.Var) (s_1 : Lean.Grind.AC.Seq),
              s' = Lean.Grind.AC.Seq.cons x_1 s_1 →
                Nat.beq x x_1 = true →
                  motive s s.eraseDup → motive (Lean.Grind.AC.Seq.cons x s) (Lean.Grind.AC.Seq.cons x_1 s_1)) →
          (∀ (x : Lean.Grind.AC.Var) (s : Lean.Grind.AC.Seq),
              have s' := s.eraseDup;
              ∀ (x_1 : Lean.Grind.AC.Var) (s_1 : Lean.Grind.AC.Seq),
                s' = Lean.Grind.AC.Seq.cons x_1 s_1 →
                  ¬Nat.beq x x_1 = true →
                    motive s s.eraseDup →
                      motive (Lean.Grind.AC.Seq.cons x s) (Lean.Grind.AC.Seq.cons x (Lean.Grind.AC.Seq.cons x_1 s_1))) →
            ∀ (s : Lean.Grind.AC.Seq), motive s s.eraseDup