mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.HasFiniteIntegral.congr' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] [inst_1 : NormedAddCommGroup γ] {f : α → β} {g : α → γ},
  MeasureTheory.HasFiniteIntegral f μ → (∀ᵐ (a : α) ∂μ, ‖f a‖ = ‖g a‖) → MeasureTheory.HasFiniteIntegral g μ
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
CategoryTheory.Limits.ReflectsFiniteCoproducts.reflects : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {F : CategoryTheory.Functor C D} [self : CategoryTheory.Limits.ReflectsFiniteCoproducts F] (n : ℕ),
  CategoryTheory.Limits.ReflectsColimitsOfShape (CategoryTheory.Discrete (Fin n)) F
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_roc_add_right_eq_map : ∀ {m n : ℕ}, (m<...=m + n).toArray = Array.map (fun x => x + m + 1) (0...n).toArray
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- A set, considered as a subset of its spanned affine subspace, spans the whole subspace.  -/
affineSpan_coe_preimage_eq_top : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (A : Set P) [inst_4 : Nonempty ↑A], affineSpan k (Subtype.val ⁻¹' A) = ⊤
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size_insertMany_list : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List (α × β)},
  List.Pairwise (fun a b => (a.1 == b.1) = false) l →
    (∀ a ∈ m, (List.map Prod.fst l).contains a = false) → (m.insertMany l).size = m.size + l.length
-- Mathlib.Combinatorics.Additive.ApproximateSubgroup
IsApproximateSubgroup.nonempty : ∀ {G : Type u_1} [inst : Group G] {A : Set G} {K : ℝ}, IsApproximateSubgroup K A → A.Nonempty
-- Lean.Data.SSet
/-- Move from stage 1 into stage 2.  -/
Lean.SSet.switch : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → Lean.SSet α → Lean.SSet α
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.coeffs_add : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : DecidableEq R] {p q : MvPolynomial σ R},
  Disjoint p.support q.support → (p + q).coeffs = p.coeffs ∪ q.coeffs
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.map_sub : ∀ {R : Type u_1} [inst : Ring R] {R₂ : Type u_2} [inst_1 : Ring R₂] {M : Type u_4} [inst_2 : TopologicalSpace M]
  [inst_3 : AddCommGroup M] {M₂ : Type u_5} [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommGroup M₂]
  [inst_6 : Module R M] [inst_7 : Module R₂ M₂] {σ₁₂ : R →+* R₂} (f : M →SL[σ₁₂] M₂) (x y : M), f (x - y) = f x - f y
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_union!_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α} [inst_1 : Inhabited (β k)],
        Std.DTreeMap.Internal.Impl.contains k m₁ = false → (m₁.union! m₂).get! k = m₂.get! k
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.GenerateMeasurable.iUnion : ∀ {α : Type u_1} {s : Set (Set α)} (f : ℕ → Set α),
  (∀ (n : ℕ), MeasurableSpace.GenerateMeasurable s (f n)) → MeasurableSpace.GenerateMeasurable s (⋃ i, f i)
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
/-- See `LinearIndependent.finSnoc'` for an uglier version that works if you
only have a module over a semiring, and `LinearIndependent.finSnoc_of_not_mem_span_over` for a
version over a subring of a division ring.  -/
LinearIndependent.finSnoc : ∀ {K : Type u_3} {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {x : V} {n : ℕ}
  {v : Fin n → V}, LinearIndependent K v → x ∉ Submodule.span K (Set.range v) → LinearIndependent K (Fin.snoc v x)
-- Mathlib.RingTheory.Artinian.Module
DivisionSemiring.instIsArtinianRing : ∀ {K : Type u_1} [inst : DivisionSemiring K], IsArtinianRing K
-- Mathlib.RingTheory.TensorProduct.DirectLimitFG
Submodule.FG.rTensor.directLimit.eq_1 : ∀ (R : Type u) (M : Type u_1) (N : Type u_2) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : DecidableEq { P // P.FG }],
  Submodule.FG.rTensor.directLimit R M N =
    (TensorProduct.directLimitLeft (fun P Q => Submodule.inclusion) N).symm.trans
      (LinearEquiv.rTensor N (Submodule.FG.directLimit R M))
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.support_tail_of_not_nil : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), ¬p.Nil → p.tail.support = p.support.tail
-- Mathlib.RingTheory.Finiteness.Defs
Submodule.fg_iff_addSubgroup_fg : ∀ {G : Type u_3} [inst : AddCommGroup G] (P : Submodule ℤ G), P.FG ↔ P.toAddSubgroup.FG
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
SimpleGraph.adjMatrix_completeGraph_eq_of_one_sub_one : ∀ (α : Type u_1) (V : Type u_2) [inst : AddGroup α] [inst_1 : One α] [inst_2 : DecidableEq V],
  SimpleGraph.adjMatrix α (SimpleGraph.completeGraph V) = Matrix.of 1 - 1
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.IndepSets.indep_aux : ∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {m₂ m : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω}
  {μ : MeasureTheory.Measure α} [ProbabilityTheory.IsZeroOrMarkovKernel κ] {p1 p2 : Set (Set Ω)},
  m₂ ≤ m →
    IsPiSystem p2 →
      m₂ = MeasurableSpace.generateFrom p2 →
        ProbabilityTheory.Kernel.IndepSets p1 p2 κ μ →
          ∀ {t1 t2 : Set Ω},
            t1 ∈ p1 → MeasurableSet t1 → MeasurableSet t2 → ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2
-- Mathlib.RingTheory.Radical.NatInt
/-- Positivity extension for radical. Proves radicals are nonzero.  -/
Nat.Mathlib.Meta.Positivity.evalRadical : Mathlib.Meta.Positivity.PositivityExt
-- Init.Data.Rat.Lemmas
Rat.natCast_pow : ∀ (a b : ℕ), ↑(a ^ b) = ↑a ^ b
-- Mathlib.CategoryTheory.Monoidal.Closed.FunctorToTypes
/-- A right adjoint of `tensorLeft F`.  -/
CategoryTheory.FunctorToTypes.rightAdj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Functor C (Type (max w v u)) →
      CategoryTheory.Functor (CategoryTheory.Functor C (Type (max w v u))) (CategoryTheory.Functor C (Type (max w v u)))
-- Mathlib.Data.Set.Pairwise.Lattice
Set.pairwise_sUnion : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set (Set α)},
  DirectedOn (fun x1 x2 => x1 ⊆ x2) s → ((⋃₀ s).Pairwise r ↔ ∀ a ∈ s, a.Pairwise r)
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Affine.Simplex.univ_centroid_eq : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} (s : Affine.Simplex k P n), Finset.centroid k Finset.univ s.points = s.centroid
-- Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
/-- Formulation of reflection formula tailored to functional equations of L-functions of even
Dirichlet characters (including Riemann zeta).  -/
Complex.inv_Gammaℝ_one_sub : ∀ {s : ℂ}, (∀ (n : ℕ), s ≠ -↑n) → (1 - s).Gammaℝ⁻¹ = s.Gammaℂ * Complex.cos (↑Real.pi * s / 2) * s.Gammaℝ⁻¹
-- Mathlib.Algebra.Lie.Cochain
LieModule.Cohomology.d₁₂.congr_simp : ∀ (R : Type u_1) [inst : CommRing R] (L : Type u_2) [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (M : Type u_3)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M],
  LieModule.Cohomology.d₁₂ R L M = LieModule.Cohomology.d₁₂ R L M
-- Mathlib.GroupTheory.Coset.Basic
AddSubgroup.quotientAddSubgroupOfMapOfLE.eq_1 : ∀ {α : Type u_1} [inst : AddGroup α] {s t : AddSubgroup α} (H : AddSubgroup α) (h : s ≤ t),
  AddSubgroup.quotientAddSubgroupOfMapOfLE H h = Quotient.map' id ⋯
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.coyonedaPairingExt : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C × CategoryTheory.Functor C (Type v₁)}
  {x y : (CategoryTheory.coyonedaPairing C).obj X}, (∀ (Y : C), x.app Y = y.app Y) → x = y
-- Mathlib.CategoryTheory.Sigma.Basic
/-- Assemble an `I`-indexed family of natural transformations into a single natural transformation.
 -/
CategoryTheory.Sigma.natTrans.sigma : {I : Type w₁} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      {D : I → Type u₁} →
        [inst_1 : (i : I) → CategoryTheory.Category.{v₁, u₁} (D i)] →
          {F G : (i : I) → CategoryTheory.Functor (C i) (D i)} →
            ((i : I) → F i ⟶ G i) → (CategoryTheory.Sigma.Functor.sigma F ⟶ CategoryTheory.Sigma.Functor.sigma G)
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.TerminationHints.none : Lean.Elab.TerminationHints
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- One line equals another differing in the first point if the first point of the first line is
contained in the second line and does not equal the second point.  -/
affineSpan_pair_eq_of_left_mem_of_ne : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {p₁ p₂ p₃ : P}, p₁ ∈ line[k, p₂, p₃] → p₁ ≠ p₃ → line[k, p₁, p₃] = line[k, p₂, p₃]
-- Lean.Elab.InfoTree.Types
Lean.Elab.DocElabInfo.toElabInfo : Lean.Elab.DocElabInfo → Lean.Elab.ElabInfo
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.Hom.s₁'.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} (f : E.Hom F) (k : E.I₁'),
  f.s₁' k = ⟨(f.s₀ k.fst.1, f.s₀ k.fst.2), f.s₁ k.snd⟩
-- Mathlib.Order.ConditionallyCompleteLattice.Finset
Multiset.iInf_mem_map_of_exists_le_sInf_empty : ∀ {ι : Type u_1} {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] {s : Multiset ι} (f : ι → α),
  (∃ x ∈ s, f x ≤ sInf ∅) → ⨅ x ∈ s, f x ∈ Multiset.map f s
-- Init.Data.AC
Lean.Data.AC.Context.unwrap_isNeutral : ∀ {α : Sort u_1} {ctx : Lean.Data.AC.Context α} {x : ℕ},
  Lean.Data.AC.ContextInformation.isNeutral ctx x = true →
    Std.LawfulIdentity (Lean.Data.AC.EvalInformation.evalOp ctx) (Lean.Data.AC.EvalInformation.evalVar ctx x)
-- Mathlib.Algebra.ContinuedFractions.Translations
GenContFract.contsAux.eq_def : ∀ {K : Type u_2} [inst : DivisionRing K] (g : GenContFract K) (x : ℕ),
  g.contsAux x =
    match x with
    | 0 => { a := 1, b := 0 }
    | 1 => { a := g.h, b := 1 }
    | n.succ.succ =>
      match g.s.get? n with
      | none => g.contsAux (n + 1)
      | some gp => GenContFract.nextConts gp.a gp.b (g.contsAux n) (g.contsAux (n + 1))
-- Mathlib.CategoryTheory.SmallObject.Construction
CategoryTheory.SmallObject.ιFunctorObj_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i)
  {S T X Y : C} {πX : X ⟶ S} {πY : Y ⟶ T} (τ : CategoryTheory.Arrow.mk πX ⟶ CategoryTheory.Arrow.mk πY)
  [inst_1 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX))
      C]
  [inst_2 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πY))
      C]
  [inst_3 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX)
      (CategoryTheory.SmallObject.functorObjLeft f πX)]
  [inst_4 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πY)
      (CategoryTheory.SmallObject.functorObjLeft f πY)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.ιFunctorObj f πX)
      (CategoryTheory.SmallObject.functorMap f τ) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left τ) (CategoryTheory.SmallObject.ιFunctorObj f πY)
-- Init.Data.BitVec.Bitblast
/-- Conjunction for fast umulOverflow circuit
 -/
BitVec.aandRec : {w : ℕ} → BitVec w → BitVec w → (s : ℕ) → s < w → Bool
-- Mathlib.Algebra.Category.Grp.Basic
/-- The category of additive groups and group morphisms.  -/
AddGrpCat : Type (u + 1)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVLogicalExpr.sat_true : ∀ {assign : Std.Tactic.BVDecide.BVExpr.Assignment},
  Std.Tactic.BVDecide.BVLogicalExpr.Sat (Std.Tactic.BVDecide.BoolExpr.const true) assign
-- Mathlib.Probability.ProductMeasure
MeasureTheory.Measure.isProjectiveLimit_infinitePiNat : ∀ {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)} (μ : (n : ℕ) → MeasureTheory.Measure (X n))
  [hμ : ∀ (n : ℕ), MeasureTheory.IsProbabilityMeasure (μ n)],
  MeasureTheory.IsProjectiveLimit (MeasureTheory.Measure.infinitePiNat μ) fun I =>
    MeasureTheory.Measure.pi fun i => μ ↑i
-- Mathlib.Algebra.Group.Prod
AddMonoidHom.snd_comp_inl : ∀ {M : Type u_3} {N : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  (AddMonoidHom.snd M N).comp (AddMonoidHom.inl M N) = 0
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.instAddCommMonoid : {R : Type u_1} → {M : Type u_4} → [inst : Semiring R] → AddCommMonoid (MonoidAlgebra R M)
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
quasispectrum.eq_1 : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalRing A] [inst_2 : Module R A] (a : A),
  quasispectrum R a = {r | ∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a))}
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
Summable.star : ∀ {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α]
  [inst_2 : StarAddMonoid α] [ContinuousStar α] {f : β → α}, Summable f L → Summable (fun b => star (f b)) L
-- Mathlib.RingTheory.Congruence.Basic
RingCon.smulCommClass' : ∀ {α : Type u_1} {R : Type u_3} [inst : Add R] [inst_1 : MulOneClass R] [inst_2 : SMul α R]
  [inst_3 : IsScalarTower α R R] [SMulCommClass R α R] (c : RingCon R), SMulCommClass c.Quotient α c.Quotient
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData.eq_1 : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  [inst_3 : X.HasSpectralSequence data] (r r' : ℤ) (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq pq' pq'' : κ)
  (hpq : (c r).prev pq' = pq) (hpq' : (c r).next pq' = pq'') (i₀' i₀ i₁ i₂ i₃ i₃' : ι) (hi₀' : i₀' = data.i₀ r' pq' ⋯)
  (hi₀ : i₀ = data.i₀ r pq' ⋯) (hi₁ : i₁ = data.i₁ pq') (hi₂ : i₂ = data.i₂ pq') (hi₃ : i₃ = data.i₃ r pq' ⋯)
  (hi₃' : i₃' = data.i₃ r' pq' ⋯) (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq') (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂),
  X.spectralSequenceHomologyData data r r' hrr' hr pq pq' pq'' hpq hpq' i₀' i₀ i₁ i₂ i₃ i₃' hi₀' hi₀ hi₁ hi₂ hi₃ hi₃' n₀
      n₁ n₂ hn₁' hn₁ hn₂ =
    CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData X data r r' hrr' hr pq pq' pq'' hpq hpq' i₀' i₀
      i₁ i₂ i₃ i₃' hi₀' hi₀ hi₁ hi₂ hi₃ hi₃' n₀ n₁ n₂ hn₁' ⋯ ⋯
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.any_eq_anyM : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Std.IteratorLoop α Id Id]
  [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β} {p : β → Bool},
  Std.Iter.any p it = (Std.Iter.anyM (fun x => pure (p x)) it).run
-- Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
/-- If `f` is complex meromorphic on a circle in the complex plane, then `log⁺ ‖f ·‖` is circle
integrable over that circle.
 -/
MeromorphicOn.circleIntegrable_posLog_norm : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {c : ℂ} {R : ℝ} {f : ℂ → E},
  MeromorphicOn f (Metric.sphere c |R|) → CircleIntegrable (fun x => ‖f x‖.posLog) c R
-- Mathlib.Algebra.Category.ModuleCat.InjectiveDimension
ModuleCat.injectiveDimension_eq_of_linearEquiv : ∀ {R : Type u} [inst : Ring R] [Small.{v, u} R] [Small.{v', u} R] {M : ModuleCat R} {N : ModuleCat R} (e : ↑M ≃ₗ[R] ↑N),
  CategoryTheory.injectiveDimension M = CategoryTheory.injectiveDimension N
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.unicodeSymbolNoAntiquot.parenthesizer : String → String → Bool → Lean.PrettyPrinter.ParenthesizerM Unit
-- Init.Data.List.Sort.Lemmas
List.mergeSort_singleton : ∀ {α : Type u_1} {r : α → α → Bool} (a : α), [a].mergeSort r = [a]
-- Aesop.Saturate
_private.Aesop.Saturate.0.Aesop.saturateCore.tryNormRules : Aesop.LocalRuleSet →
  Lean.MVarId → Aesop.UnorderedArraySet Lean.MVarId → Lean.Meta.SavedState → Aesop.SaturateM (Option Aesop.GoalDiff)
-- Lean.Compiler.IR.Basic
Lean.IR.IRType.brecOn_1.go : {motive_1 : Lean.IR.IRType → Sort u} →
  {motive_2 : Array Lean.IR.IRType → Sort u} →
    {motive_3 : List Lean.IR.IRType → Sort u} →
      (t : Array Lean.IR.IRType) →
        ((t : Lean.IR.IRType) → t.below → motive_1 t) →
          ((t : Array Lean.IR.IRType) → Lean.IR.IRType.below_1 t → motive_2 t) →
            ((t : List Lean.IR.IRType) → Lean.IR.IRType.below_2 t → motive_3 t) → motive_2 t ×' Lean.IR.IRType.below_1 t
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.condExpL1_undef : ∀ {α : Type u_1} {F' : Type u_3} [inst : NormedAddCommGroup F'] [inst_1 : NormedSpace ℝ F'] {m m0 : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {hm : m ≤ m0} [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)] {f : α → F'},
  ¬MeasureTheory.Integrable f μ → MeasureTheory.condExpL1 hm μ f = 0
-- Mathlib.Order.Comparable
instReflIncompRelOfIrrefl : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Irrefl r], Std.Refl (IncompRel r)
-- Mathlib.Tactic.FunProp.Types
/-- It is a free variable in the local context.  -/
Mathlib.Meta.FunProp.Origin.fvar : Lean.FVarId → Mathlib.Meta.FunProp.Origin
-- Mathlib.Algebra.Homology.Embedding.TruncGE
/-- The `X` field of `truncGE'`.  -/
HomologicalComplex.truncGE'.X : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
              (K : HomologicalComplex C c') → c.Embedding c' → [∀ (i' : ι'), K.HasHomology i'] → ι → C
-- Init.Data.Array.Count
Array.count_push_self : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {xs : Array α}, Array.count a (xs.push a) = Array.count a xs + 1
-- Mathlib.SetTheory.ZFC.Basic
/-- Graph of a function: `map f x` is the ZFC function which maps `a ∈ x` to `f a`  -/
ZFSet.map : (f : ZFSet.{u_1} → ZFSet.{u_1}) → [ZFSet.Definable₁ f] → ZFSet.{u_1} → ZFSet.{u_1}
-- Mathlib.Algebra.Order.Group.Lattice
inf_div : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] [MulRightMono α] (a b c : α), (a ⊓ b) / c = a / c ⊓ b / c
-- Mathlib.Data.NNReal.Basic
NNReal.image_coe_Iic : ∀ (x : NNReal), NNReal.toReal '' Set.Iic x = Set.Icc 0 ↑x
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.Point.toAffine_of_equiv : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P Q : Fin 3 → F},
  P ≈ Q → WeierstrassCurve.Projective.Point.toAffine W P = WeierstrassCurve.Projective.Point.toAffine W Q
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKey?_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α fun x => Unit} [EquivBEq α] [LawfulHashable α]
  {l : List α} {k : α}, k ∈ m → (Std.DHashMap.Const.insertManyIfNewUnit m l).getKey? k = m.getKey? k
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.card_zero : Ordinal.card 0 = 0
-- Mathlib.Order.LatticeIntervals
/-- `Ioc a b` has a top element whenever `a < b`.  -/
Set.Ioc.orderTop : {α : Type u_1} → [inst : PartialOrder α] → {a b : α} → [Fact (a < b)] → OrderTop ↑(Set.Ioc a b)
-- Mathlib.CategoryTheory.Core
CategoryTheory.Equivalence.core_functor_map_iso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : C ≌ D) {X Y : CategoryTheory.Core C} (f : X ⟶ Y), (E.core.functor.map f).iso.hom = E.functor.map f.iso.hom
-- Mathlib.Data.Matrix.Mul
Matrix.vecMulVec_zero : ∀ {m : Type u_2} {α : Type v} [inst : MulZeroClass α] (w : m → α), Matrix.vecMulVec w 0 = 0
-- Mathlib.Data.Holor
HolorIndex.drop_drop : ∀ {ds₁ ds₂ ds₃ : List ℕ} (t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)), t.assocRight.drop.drop = t.drop
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.δ_comp_σ_succ' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ}
  {j : Fin (n + 2)} {i : Fin (n + 1)},
  j = i.succ →
    CategoryTheory.CategoryStruct.comp (X.σ i) (X.δ j) =
      CategoryTheory.CategoryStruct.id (X.obj (Opposite.op { len := n }))
-- Mathlib.Analysis.Complex.RealDeriv
HasDerivAt.complexToReal_fderiv' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {x : ℂ} {f' : E},
  HasDerivAt f f' x → HasFDerivAt f (Complex.reCLM.smulRight f' + Complex.I • Complex.imCLM.smulRight f') x
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- The cosine of an angle in a right-angled triangle multiplied by the hypotenuse equals the
adjacent side, version subtracting vectors.  -/
Orientation.cos_oangle_sub_left_mul_norm_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑(Real.pi / 2) → (o.oangle (x - y) x).cos * ‖x - y‖ = ‖x‖
-- Mathlib.Analysis.Convex.Side
AffineSubspace.isConnected_setOfPred_sOppSide : ∀ {V : Type u_2} {P : Type u_4} [inst : SeminormedAddCommGroup V] [inst_1 : NormedSpace ℝ V]
  [inst_2 : PseudoMetricSpace P] [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} {x : P},
  x ∉ s → (↑s).Nonempty → IsConnected {y | s.SOppSide x y}
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.get?_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] {k : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.get? k = t₂.get? k
-- Lean.Meta.KExprMap
Lean.Meta.KExprMap.mk.inj : ∀ {α : Type} {map map_1 : Lean.PHashMap Lean.HeadIndex (Lean.AssocList Lean.Expr α)},
  { map := map } = { map := map_1 } → map = map_1
-- Mathlib.Algebra.Category.Grp.Basic
/-- Construct a bundled `CommGrpCat` from the underlying type and typeclass.  -/
CommGrpCat.of : (M : Type u) → [CommGroup M] → CommGrpCat
-- Mathlib.Data.List.TakeWhile
List.takeWhile_eq_self_iff : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, List.takeWhile p l = l ↔ ∀ x ∈ l, p x = true
-- Lean.Meta.Tactic.Grind.Split
/-- Given `e` of the form `@Eq Prop a b`, check whether we are ready to case-split on `e`.
There are two cases:
1- `e` is `True`, but neither both `a` and `b` are `True`, nor both `a` and `b` are `False`.
2- `e` is `False`, but neither `a` is `True` and `b` is `False`, nor `a` is `False` and `b` is `True`.
 -/
_private.Lean.Meta.Tactic.Grind.Split.0.Lean.Meta.Grind.checkIffStatus : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Lean.Meta.Grind.SplitStatus
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.instAdd.eq_1 : ∀ {α : Type u} [inst : Add α], WithZero.instAdd = { add := Option.merge fun x1 x2 => x1 + x2 }
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RooSliceData.mk.sizeOf_spec : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : SizeOf α] [inst_2 : (a : α) → SizeOf (β a)]
  (treeMap : Std.DTreeMap.Internal.Impl α β) (range : Std.Roo α),
  sizeOf { treeMap := treeMap, range := range } = 1 + sizeOf treeMap + sizeOf range
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
CategoryTheory.CostructuredArrow.map.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T T' : D} {S : CategoryTheory.Functor C D} (f : T ⟶ T'),
  CategoryTheory.CostructuredArrow.map f =
    CategoryTheory.Comma.mapRight S ((CategoryTheory.Functor.const (CategoryTheory.Discrete PUnit.{1})).map f)