mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskeringLeft₂_map_app_app_app_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D₂] (E : Type u_7) [inst_4 : CategoryTheory.Category.{v_7, u_7} E]
  {X Y : CategoryTheory.Functor C₁ D₁} (ψ : X ⟶ Y) (F₂ : CategoryTheory.Functor C₂ D₂)
  (X_1 : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ E)) (c : C₁) (X_2 : C₂),
  (((((CategoryTheory.Functor.whiskeringLeft₂ E).map ψ).app F₂).app X_1).app c).app X_2 =
    (X_1.map (ψ.app c)).app (F₂.obj X_2)
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
padicValNat_dvd_iff_of_ne_one : ∀ {p : ℕ}, p ≠ 1 → ∀ (n a : ℕ), p ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValNat p a
-- Mathlib.Algebra.Ring.Aut
RingAut.mul_apply : ∀ {R : Type u_1} [inst : Mul R] [inst_1 : Add R] (f g : R ≃+* R) (x : R), (f * g) x = f (g x)
-- Mathlib.Tactic.Widget.CommDiag
/-- Given a commutative square `f ≫ g = i ≫ h`, return a square diagram. Otherwise `none`.  -/
Mathlib.Tactic.Widget.commSquareM? : Lean.Expr → Lean.MetaM (Option ProofWidgets.Html)
-- Mathlib.RingTheory.SurjectiveOnStalks
/-- A ring homomorphism `R →+* S` is surjective on stalks if `R_p →+* S_q` is surjective for all pairs
of primes `p = f⁻¹(q)`.
 -/
RingHom.SurjectiveOnStalks : {R : Type u_1} → [inst : CommRing R] → {S : Type u_2} → [inst_1 : CommRing S] → (R →+* S) → Prop
-- Mathlib.GroupTheory.Congruence.Defs
Con.toSetoid_eq_top : ∀ {M : Type u_1} [inst : Mul M] {c : Con M}, c.toSetoid = ⊤ ↔ c = ⊤
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
AlgebraicGeometry.ExistsHomHomCompEqCompAux.hb : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] {S X : AlgebraicGeometry.Scheme}
  {D : CategoryTheory.Functor I AlgebraicGeometry.Scheme} {t : D ⟶ (CategoryTheory.Functor.const I).obj S} {f : X ⟶ S}
  (self : AlgebraicGeometry.ExistsHomHomCompEqCompAux D t f), t.app self.i = CategoryTheory.CategoryStruct.comp self.b f
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.addImportedFn : {α β σ : Type} →
  Lean.ScopedEnvExtension.Descr α β σ →
    Array (Array (Lean.ScopedEnvExtension.Entry α)) → Lean.ImportM (Lean.ScopedEnvExtension.StateStack α β σ)
-- Std.Data.Internal.List.Associative
Std.Internal.List.foldr_eq_foldr_keys : ∀ {α : Type u} {β : α → Type v} {δ : Type w} {l : List ((a : α) × β a)} {f : α → δ → δ} {init : δ},
  List.foldr (fun a b => f a.fst b) init l = List.foldr f init (Std.Internal.List.keys l)
-- Mathlib.NumberTheory.LSeries.Linearity
LSeries.term_neg_apply : ∀ (f : ℕ → ℂ) (s : ℂ) (n : ℕ), LSeries.term (-f) s n = -LSeries.term f s n
-- Init.Data.Fin.Lemmas
Fin.natAdd_castSucc : ∀ {m n : ℕ} {i : Fin m}, Fin.natAdd n i.castSucc = (Fin.natAdd n i).castSucc
-- Init.Data.Nat.Lemmas
Nat.exists_ne_zero : ∀ {P : ℕ → Prop}, (∃ n, ¬n = 0 ∧ P n) ↔ ∃ n, P (n + 1)
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
/-- Being a closed immersion is local at the target.  -/
AlgebraicGeometry.IsClosedImmersion.isZariskiLocalAtTarget : AlgebraicGeometry.IsZariskiLocalAtTarget @AlgebraicGeometry.IsClosedImmersion
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
_private.Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno.0.Fin.succ.match_1.eq_1 : ∀ {n : ℕ} (motive : Fin n → Sort u_1) (i : ℕ) (h : i < n) (h_1 : (i : ℕ) → (h : i < n) → motive ⟨i, h⟩),
  (match ⟨i, h⟩ with
    | ⟨i, h⟩ => h_1 i h) =
    h_1 i h
-- Mathlib.Data.FunLike.Group
FunLike.addZeroClass.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Add F] [inst_2 : Zero F]
  [inst_3 : AddZeroClass β] [inst_4 : IsZeroApply F α β] [inst_5 : IsAddApply F α β],
  FunLike.addZeroClass = Function.Injective.addZeroClass (fun f => ⇑f) ⋯ ⋯ ⋯
-- Mathlib.Order.WithBot
WithTop.untopD_top : ∀ {α : Type u_5} (d : α), WithTop.untopD d ⊤ = d
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
LinearOrderedCommMonoidWithZero.toCommMonoidWithZero : {α : Type u_3} → [self : LinearOrderedCommMonoidWithZero α] → CommMonoidWithZero α
-- Mathlib.LinearAlgebra.Dimension.Basic
/-- The same-universe version of `Algebra.lift_rank_le_of_injective_injective`.  -/
Algebra.rank_le_of_injective_injective : ∀ {R : Type w} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {R' : Type w'}
  [inst_3 : CommSemiring R'] {S' : Type v} [inst_4 : Semiring S'] [inst_5 : Algebra R' S'] (i : R' →+* R)
  (j : S →+* S'),
  Function.Injective ⇑i →
    Function.Injective ⇑j → (j.comp (algebraMap R S)).comp i = algebraMap R' S' → Module.rank R S ≤ Module.rank R' S'
-- Mathlib.RepresentationTheory.Invariants
Representation.linHom.invariantsEquivRepHom_apply : ∀ {k : Type u} [inst : CommRing k] {G : Type v} [inst_1 : Group G] (X Y : Rep.{w, u, v} k G)
  (f : ↥(X.ρ.linHom Y.ρ).invariants),
  (Representation.linHom.invariantsEquivRepHom X Y) f = Rep.ofHom { toLinearMap := ↑f, isIntertwining' := ⋯ }
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
/-- The natural transformation that is part of a morphism between spectral objects.  -/
CategoryTheory.Triangulated.SpectralObject.Hom.hom : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] →
        [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
          [inst_3 : CategoryTheory.HasShift C ℤ] →
            [inst_4 : CategoryTheory.Preadditive C] →
              [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
                [inst_6 : CategoryTheory.Pretriangulated C] →
                  {X Y : CategoryTheory.Triangulated.SpectralObject C ι} → X.Hom Y → (X.ω₁ ⟶ Y.ω₁)
-- Std.Internal.Do.Order.Basic
/-- `⌜p⌝ ⊑ rhs` reduces to assuming `p` and proving `⊤ ⊑ rhs`.  -/
Lean.Order.ofProp_le : ∀ {l : Type u_1} [inst : Lean.Order.CompleteLattice l] (p : Prop) (rhs : l),
  (p → Lean.Order.PartialOrder.rel Lean.Order.top rhs) →
    Lean.Order.PartialOrder.rel (Lean.Order.CompleteLattice.ofProp p) rhs
-- Mathlib.MeasureTheory.Integral.TorusIntegral
TorusIntegrable.torusIntegrable_zero_radius : ∀ {n : ℕ} {E : Type u_1} [inst : NormedAddCommGroup E] {f : (Fin n → ℂ) → E} {c : Fin n → ℂ}, TorusIntegrable f c 0
-- Mathlib.RingTheory.Morita.Basic
/-- For any `R`-algebra `A`, `A` is Morita equivalent to itself.
 -/
MoritaEquivalence.refl : (R : Type u₀) →
  [inst : CommSemiring R] → (A : Type u₁) → [inst_1 : Ring A] → [inst_2 : Algebra R A] → MoritaEquivalence R A A
-- Mathlib.RingTheory.PowerSeries.Order
PowerSeries.X_pow_order_mul_divXPowOrder : ∀ {R : Type u_1} [inst : Semiring R] {f : PowerSeries R}, PowerSeries.X ^ f.order.toNat * f.divXPowOrder = f
-- Lean.Util.CollectMVars
Lean.CollectMVars.State.mk.injEq : ∀ (visitedExpr : Lean.ExprSet) (result : Array Lean.MVarId) (visitedExpr_1 : Lean.ExprSet)
  (result_1 : Array Lean.MVarId),
  ({ visitedExpr := visitedExpr, result := result } = { visitedExpr := visitedExpr_1, result := result_1 }) =
    (visitedExpr = visitedExpr_1 ∧ result = result_1)
-- Mathlib.Data.Nat.Hyperoperation
hyperoperation_two : ∀ (m k : ℕ), hyperoperation 2 m k = m * k
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.mapRange_surjective : ∀ {ι : Type u} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [inst : (i : ι) → Zero (β₁ i)] [inst_1 : (i : ι) → Zero (β₂ i)]
  (f : (i : ι) → β₁ i → β₂ i) (hf : ∀ (i : ι), f i 0 = 0),
  Function.Surjective (DFinsupp.mapRange f hf) ↔ ∀ (i : ι), Function.Surjective (f i)
-- Mathlib.GroupTheory.Congruence.Defs
AddConGen.Rel.below.of : ∀ {M : Type u_1} [inst : Add M] {r : M → M → Prop} {motive : (a a_1 : M) → AddConGen.Rel r a a_1 → Prop} (x y : M)
  (a : r x y), AddConGen.Rel.below ⋯
-- Mathlib.Topology.MetricSpace.Pseudo.Pi
/-- An open ball in a product space is a product of open balls. See also `ball_pi`
for a version assuming `0 < r` instead of `Nonempty β`.  -/
ball_pi' : ∀ {β : Type u_2} {X : β → Type u_3} [inst : Fintype β] [inst_1 : (b : β) → PseudoMetricSpace (X b)] [Nonempty β]
  (x : (b : β) → X b) (r : ℝ), Metric.ball x r = Set.univ.pi fun b => Metric.ball (x b) r
-- Init.Data.Nat.Lemmas
Nat.log2_lt : ∀ {n k : ℕ}, n ≠ 0 → (n.log2 < k ↔ n < 2 ^ k)
-- Mathlib.Topology.Algebra.IntermediateField
IntermediateField.continuousSMul : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [inst_3 : TopologicalSpace L]
  (X : Type u_3) [inst_4 : TopologicalSpace X] [inst_5 : MulAction L X] [ContinuousSMul L X]
  (M : IntermediateField K L), ContinuousSMul (↥M) X
-- Mathlib.Order.Filter.AtTopBot.Finset
/-- The pushforward of `atTop` on `Finset α` along `Finset.card` is `pure (Fintype.card α)`, when
`α` is finite.  -/
Filter.map_card_atTop_of_fintype : ∀ {α : Type u_3} [inst : Fintype α], Filter.map Finset.card Filter.atTop = pure (Fintype.card α)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.reachable_is_equivalence : ∀ {V : Type u} (G : SimpleGraph V), Equivalence G.Reachable
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.ring : {R : Type u} →
  {M : Type v} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → [inst_3 : Module Rᵐᵒᵖ M] → [SMulCommClass R Rᵐᵒᵖ M] → Ring (TrivSqZeroExt R M)
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instAddMonoid : {α : Type u_1} → [AddMonoid α] → AddMonoid αᵃᵒᵖ
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint_preserves_motive : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (rupHints : Array ℕ) (idx : Fin rupHints.size)
  (acc :
    Array Std.Tactic.BVDecide.LRAT.Internal.Assignment ×
      Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) × Bool × Bool),
  f.ConfirmRupHintFoldEntailsMotive (↑idx) acc →
    f.ConfirmRupHintFoldEntailsMotive (↑idx + 1)
      (Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint f.clauses acc rupHints[idx])
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Term.realize_subst : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {β : Type v'} {t : L.Term α}
  {tf : α → L.Term β} {v : β → M},
  FirstOrder.Language.Term.realize v (t.subst tf) =
    FirstOrder.Language.Term.realize (fun a => FirstOrder.Language.Term.realize v (tf a)) t
-- Mathlib.SetTheory.Ordinal.Notation
ONote.NF.fst : ∀ {e : ONote} {n : ℕ+} {a : ONote}, (e.oadd n a).NF → e.NF
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.unitOfList_nil : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α}, Std.DHashMap.Const.unitOfList [] = ∅
-- Mathlib.Order.Basic
eq_iff_le_not_lt : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α}, a = b ↔ a ≤ b ∧ ¬a < b
-- Batteries.Data.List.Perm
List.Perm.diff : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {l₁ l₂ t₁ t₂ : List α},
  l₁.Perm l₂ → t₁.Perm t₂ → (l₁.diff t₁).Perm (l₂.diff t₂)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.mem_of_mem_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∈ m₁ ∪ m₂ → k ∉ m₁ → k ∈ m₂
-- Mathlib.Analysis.Normed.Group.SeparationQuotient
/-- The operator norm of the projection is at most `1`.  -/
SeparationQuotient.norm_normedMk_le : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M], ‖SeparationQuotient.normedMk‖ ≤ 1
-- Mathlib.Order.Filter.Basic
Filter.ker.eq_1 : ∀ {α : Type u_1} (f : Filter α), f.ker = ⋂₀ f.sets
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.DayConvolutionUnit.instIsLeftKanExtensionProdDiscretePUnitExternalProductExtensionUnitRightφ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  (U : CategoryTheory.Functor C V) [inst_4 : CategoryTheory.MonoidalCategory.DayConvolutionUnit U]
  (F : CategoryTheory.Functor C V)
  [∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)],
  (CategoryTheory.MonoidalCategory.externalProduct F U).IsLeftKanExtension
    (CategoryTheory.MonoidalCategory.ExternalProduct.extensionUnitRight U
      (CategoryTheory.MonoidalCategory.DayConvolutionUnit.φ U) F)
-- Mathlib.Order.Antichain
IsAntichain.preimage_iso : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] {t : Set β},
  IsAntichain (fun x1 x2 => x1 ≤ x2) t → ∀ (φ : α ≃o β), IsAntichain (fun x1 x2 => x1 ≤ x2) (⇑φ ⁻¹' t)
-- Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
ContMDiffOn.clm_prodMap : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F₁ : Type u_8} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_9} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {F₃ : Type u_10} [inst_10 : NormedAddCommGroup F₃] [inst_11 : NormedSpace 𝕜 F₃] {F₄ : Type u_11}
  [inst_12 : NormedAddCommGroup F₄] [inst_13 : NormedSpace 𝕜 F₄] {n : WithTop ℕ∞} {g : M → F₁ →L[𝕜] F₃}
  {f : M → F₂ →L[𝕜] F₄} {s : Set M},
  ContMDiffOn I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₃)) n g s →
    ContMDiffOn I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₄)) n f s →
      ContMDiffOn I (modelWithCornersSelf 𝕜 (F₁ × F₂ →L[𝕜] F₃ × F₄)) n (fun x => (g x).prodMap (f x)) s
-- Mathlib.Topology.Homeomorph.Lemmas
IsHomeomorph.isClosedMap : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsHomeomorph f → IsClosedMap f
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.measure_preimage_vadd_of_nullMeasurableSet : ∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : VAdd G α] {μ : MeasureTheory.Measure α}
  [MeasureTheory.VAddInvariantMeasure G α μ] {s : Set α},
  MeasureTheory.NullMeasurableSet s μ → ∀ (c : G), μ ((fun x => c +ᵥ x) ⁻¹' s) = μ s
-- Mathlib.Geometry.Manifold.Algebra.Monoid
instAddMonoidHomClassContMDiffAddMonoidMorphism : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [inst_1 : TopologicalSpace H]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : AddMonoid G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] {H' : Type u_5}
  [inst_7 : TopologicalSpace H'] {E' : Type u_6} [inst_8 : NormedAddCommGroup E'] [inst_9 : NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'} {G' : Type u_7} [inst_10 : AddMonoid G'] [inst_11 : TopologicalSpace G']
  [inst_12 : ChartedSpace H' G'], AddMonoidHomClass (ContMDiffAddMonoidMorphism I I' n G G') G G'
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.denote'.go : Int.Internal.Linear.Context → Int.Internal.Linear.Poly → ℤ → ℤ
-- Init.Data.BitVec.Lemmas
BitVec.flattenList.eq_def : ∀ {n : ℕ} (xs : List (BitVec n)),
  BitVec.flattenList xs =
    match xs with
    | [] => 0#0
    | x :: rest =>
      have h := ⋯;
      BitVec.cast h (x ++ BitVec.flattenList rest)
-- Mathlib.Algebra.Category.CommAlgCat.FiniteType
Algebra.FiniteType.exists_fgAlgCatSkeleton : ∀ (R : Type u) [inst : CommRing R] (A : Type v) [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [h : Algebra.FiniteType R A], ∃ P, Nonempty (A ≃ₐ[R] ↑(FGAlgCatSkeleton.eval R P).obj)
-- Mathlib.Data.Nat.Choose.Basic
Nat.choose_succ_self : ∀ (n : ℕ), n.choose n.succ = 0
-- Lean.Elab.Tactic.BuiltinTactic
_private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalRunTac.unsafe_1 : Lean.TSyntax `term → Lean.Elab.TermElabM (Lean.Elab.Tactic.TacticM Unit)
-- Mathlib.Algebra.Group.Submonoid.Basic
Submonoid.mem_sInf : ∀ {M : Type u_1} [inst : MulOneClass M] {S : Set (Submonoid M)} {x : M}, x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.dblX_of_Y_eq : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} [NoZeroDivisors R] {P Q : Fin 3 → R},
  Q 2 ≠ 0 →
    P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2 →
      P 1 * Q 2 ^ 3 = Q 1 * P 2 ^ 3 → P 1 * Q 2 ^ 3 = W'.negY Q * P 2 ^ 3 → W'.dblX P = W'.dblU P ^ 2
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Localization.liftOn₂.eq_1 : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {p : Sort u} (x y : Localization S) (f : M → ↥S → M → ↥S → p)
  (H :
    ∀ {a a' : M} {b b' : ↥S} {c c' : M} {d d' : ↥S},
      (Localization.r S) (a, b) (a', b') → (Localization.r S) (c, d) (c', d') → f a b c d = f a' b' c' d'),
  x.liftOn₂ y f H = x.liftOn (fun a b => y.liftOn (f a b) ⋯) ⋯
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
CategoryTheory.InjectiveResolution.descHomotopyZeroOne.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {Y Z : C}
  {I : CategoryTheory.InjectiveResolution Y} {J : CategoryTheory.InjectiveResolution Z}
  (f f_1 : I.cocomplex ⟶ J.cocomplex) (e_f : f = f_1) (comm : CategoryTheory.CategoryStruct.comp I.ι f = 0),
  CategoryTheory.InjectiveResolution.descHomotopyZeroOne f comm =
    CategoryTheory.InjectiveResolution.descHomotopyZeroOne f_1 ⋯
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.ext_iff' : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ η : ProbabilityTheory.Kernel α β},
  κ = η ↔ ∀ (a : α) (s : Set β), MeasurableSet s → (κ a) s = (η a) s
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.toOplax_mapId : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C) (a : B), F.toOplax.mapId a = (F.mapId a).hom
-- Mathlib.RingTheory.Smooth.Field
Algebra.FormallySmooth.of_perfectField : ∀ {K : Type u_1} {L : Type u_2} [inst : Field L] [inst_1 : Field K] [inst_2 : Algebra K L] [PerfectField K]
  [Algebra.EssFiniteType K L], Algebra.FormallySmooth K L
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
EisensteinSeries.summable_e2Summand_symmetricIco : ∀ (z : UpperHalfPlane), Summable (fun x => EisensteinSeries.e2Summand x z) (SummationFilter.symmetricIco ℤ)
-- Lean.Compiler.IR.Basic
Lean.IR.instBEqVarId.beq : Lean.IR.VarId → Lean.IR.VarId → Bool
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.toMulDivCancelClass : ∀ {R : Type u} [inst : EuclideanDomain R], MulDivCancelClass R
-- Mathlib.CategoryTheory.Action.Concrete
/-- If `X` is a type with `[Fintype X]` and `G` acts on `X`, then `G` also acts on
`FintypeCat.of X`.  -/
Action.FintypeCat.instMulActionObjFiniteOf : (G : Type u_1) →
  (X : Type u_2) → [inst : Monoid G] → [MulAction G X] → [inst_2 : Fintype X] → MulAction G (FintypeCat.of X).obj
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.principalUnitGroupEquiv_apply : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) (a : ↥A.principalUnitGroup),
  ↑↑↑(A.principalUnitGroupEquiv a) = ↑↑a
-- Mathlib.Data.Part
/-- `Part` eta expansion  -/
Part.eta : ∀ {α : Type u_1} (o : Part α), { Dom := o.Dom, get := fun h => o.get h } = o
-- Mathlib.Probability.Kernel.Composition.MeasureComp
MeasureTheory.Measure.copy_comp_map : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {f : α → β},
  AEMeasurable f μ →
    (MeasureTheory.Measure.map f μ).bind ⇑(ProbabilityTheory.Kernel.copy β) =
      MeasureTheory.Measure.map (Function.prod f f) μ
-- Plausible.Functions
/-- Shrink a total function by shrinking the lists that represent it.  -/
Plausible.TotalFunction.shrink : {α : Type u_1} →
  {β : Type u_2} →
    [DecidableEq α] →
      [Plausible.Shrinkable α] →
        [Plausible.Shrinkable β] → Plausible.TotalFunction α β → List (Plausible.TotalFunction α β)
-- Mathlib.RingTheory.Congruence.Hom
RingCon.comapQuotientEquivRange_symm_mk : ∀ {M : Type u_1} {N : Type u_2} [inst : Ring M] [inst_1 : Ring N] (c : RingCon M) (f : N →+* M) {d : RingCon N}
  (hcd : d = c.comap f) (x : N), (c.comapQuotientEquivRange f hcd).symm ⟨↑(f x), ⋯⟩ = ↑x
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.eq_empty_iff_size_eq_zero : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], m = ∅ ↔ m.size = 0
-- Mathlib.Algebra.Group.Basic
sub_neg_eq_add : ∀ {α : Type u_1} [inst : SubtractionMonoid α] (a b : α), a - -b = a + b
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.instHasForget₂FiniteGrpMonoidHomCarrierToGrpContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite.eq_1 : ProfiniteGrp.instHasForget₂FiniteGrpMonoidHomCarrierToGrpContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite =
  {
    forget₂ :=
      { obj := ProfiniteGrp.ofFiniteGrp, map := fun {X Y} => ProfiniteGrp.ofFiniteGrpHom,
        map_id :=
          ProfiniteGrp.instHasForget₂FiniteGrpMonoidHomCarrierToGrpContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite._proof_1,
        map_comp :=
          @ProfiniteGrp.instHasForget₂FiniteGrpMonoidHomCarrierToGrpContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite._proof_2 },
    forget_comp :=
      ProfiniteGrp.instHasForget₂FiniteGrpMonoidHomCarrierToGrpContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite._proof_4 }
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.prodMap_apply : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_5} {δ : Type u_6} [inst : VAdd M α]
  [inst_1 : VAdd M β] [inst_2 : VAdd N γ] [inst_3 : VAdd N δ] {σ : M → N} (f : α →ₑ[σ] γ) (g : β →ₑ[σ] δ),
  ⇑(f.prodMap g) = Prod.map ⇑f ⇑g
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.CaseTrace.expr : Lean.Meta.Grind.CaseTrace → Lean.Expr
-- Mathlib.Topology.Separation.Regular
Topology.IsEmbedding.t25Space : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T25Space Y] {f : X → Y},
  Topology.IsEmbedding f → T25Space X
-- Mathlib.Data.Finsupp.Option
Finsupp.optionEquiv_apply : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] (P : Option α →₀ M), Finsupp.optionEquiv P = (P none, P.some)
-- Init.Data.Fin.Lemmas
Fin.addCases_left : ∀ {m n : ℕ} {motive : Fin (m + n) → Sort u_1} {left : (i : Fin m) → motive (Fin.castAdd n i)}
  {right : (i : Fin n) → motive (Fin.natAdd m i)} (i : Fin m), Fin.addCases left right (Fin.castAdd n i) = left i
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_keysArray : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  m.keysArray.size = m.size
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Cell.alter.match_1.eq_2 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : Option ((a : α) × β a) → Sort u_3) (k' : α) (v' : β k')
  (h_1 : some ⟨k', v'⟩ = none → motive none)
  (h_2 : (k'_1 : α) → (v'_1 : β k'_1) → some ⟨k', v'⟩ = some ⟨k'_1, v'_1⟩ → motive (some ⟨k'_1, v'_1⟩)),
  (match h : some ⟨k', v'⟩ with
    | none => h_1 h
    | some ⟨k'_1, v'_1⟩ => h_2 k'_1 v'_1 h) =
    h_2 k' v' ⋯
-- Mathlib.MeasureTheory.Group.FoelnerFilter
isFoelner_iff : ∀ (G : Type u_1) {X : Type u_2} [inst : MeasurableSpace X] (μ : MeasureTheory.Measure X) [inst_1 : Group G]
  [inst_2 : MulAction G X] {ι : Type u_3} (l : Filter ι) (F : ι → Set X),
  IsFoelner G μ l F ↔
    (∀ᶠ (i : ι) in l, MeasurableSet (F i)) ∧
      (∀ᶠ (i : ι) in l, μ (F i) ≠ 0) ∧
        (∀ᶠ (i : ι) in l, μ (F i) ≠ ⊤) ∧
          ∀ (g : G), Filter.Tendsto (fun i => μ (symmDiff (g • F i) (F i)) / μ (F i)) l (nhds 0)
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.isPrefixOf.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (x : List α) (h_1 : (x : List α) → motive [] x)
  (h_2 : (x : List α) → motive x [])
  (h_3 : (a : α) → (as : List α) → (b : α) → (bs : List α) → motive (a :: as) (b :: bs)),
  (match [], x with
    | [], x => h_1 x
    | x, [] => h_2 x
    | a :: as, b :: bs => h_3 a as b bs) =
    h_1 x
-- Mathlib.Order.Fin.Basic
Fin.rev_strictAnti : ∀ {n : ℕ}, StrictAnti Fin.rev