mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.Internal.HashesTo
Std.DHashMap.Internal.List.hashesTo_nil : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {i size : ℕ},
  Std.DHashMap.Internal.List.HashesTo [] i size
-- Mathlib.Data.Finset.MulAntidiagonal
/-- `Finset.mulAntidiagonal hs ht a` is the set of all pairs of an element in `s` and an
element in `t` that multiply to `a`, but its construction requires proofs that `s` and `t` are
well-ordered.  -/
Finset.mulAntidiagonal : {α : Type u_1} →
  [inst : CommMonoid α] →
    [inst_1 : PartialOrder α] → [IsOrderedCancelMonoid α] → {s t : Set α} → s.IsPWO → t.IsPWO → α → Finset (α × α)
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.RightLift.whisker_lift : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  (t : CategoryTheory.Bicategory.RightLift f g) {x : B} (h : x ⟶ c),
  (t.whisker h).lift = CategoryTheory.CategoryStruct.comp h t.lift
-- Mathlib.RingTheory.FiniteLength
isFiniteLength_of_exists_compositionSeries : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  (∃ s, RelSeries.head s = ⊥ ∧ RelSeries.last s = ⊤) → IsFiniteLength R M
-- Lean.Parser.Basic
Lean.Parser.many1Unbox : Lean.Parser.Parser → Lean.Parser.Parser
-- Std.Data.ExtTreeSet.Basic
/-- Creates a new empty tree set. It is also possible and recommended to
use the empty collection notations `∅` and `{}` to create an empty tree set. `simp` replaces
`empty` with `∅`.
 -/
Std.ExtTreeSet.empty : {α : Type u} → {cmp : α → α → Ordering} → Std.ExtTreeSet α cmp
-- Mathlib.Algebra.Free
AddMagma.FreeAddSemigroup.lift_of : ∀ {α : Type u} [inst : Add α] {β : Type v} [inst_1 : AddSemigroup β] (f : α →ₙ+ β) (x : α),
  (AddMagma.FreeAddSemigroup.lift f) (AddMagma.FreeAddSemigroup.of x) = f x
-- Mathlib.Order.RelSeries
/-- A relation `r` is said to be infinite dimensional iff there exists relation series of
arbitrary length.  -/
SetRel.InfiniteDimensional.exists_relSeries_with_length : ∀ {α : Type u_1} {r : SetRel α α} [self : r.InfiniteDimensional] (n : ℕ), ∃ x, x.length = n
-- Mathlib.Algebra.Group.Hom.Defs
map_comp_sub' : ∀ {ι : Type u_1} {G : Type u_7} {H : Type u_8} {F : Type u_9} [inst : FunLike F G H] [inst_1 : SubNegMonoid G]
  [inst_2 : SubNegMonoid H] [AddHomClass F G H] (f : F),
  (∀ (a : G), f (-a) = -f a) → ∀ (g h : ι → G), ⇑f ∘ (g - h) = ⇑f ∘ g - ⇑f ∘ h
-- Init.Data.List.BasicAux
List.lex_trichotomous : ∀ {α : Type u_1} [DecidableEq α] {r : α → α → Prop} [DecidableRel r],
  (∀ (x y : α), ¬r x y → ¬r y x → x = y) → ∀ {as bs : List α}, ¬List.Lex r bs as → ¬List.Lex r as bs → as = bs
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.hasFiniteProducts_of_opposite : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasFiniteCoproducts Cᵒᵖ],
  CategoryTheory.Limits.HasFiniteProducts C
-- Lean.Elab.ParseImportsFast
Lean.ParseImports.State.badModifier : Lean.ParseImports.State → Bool
-- Mathlib.AlgebraicTopology.DoldKan.Decomposition
AlgebraicTopology.DoldKan.MorphComponents.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {X : CategoryTheory.SimplicialObject C} {n : ℕ} {Z : C}
  {a : X.obj (Opposite.op { len := n + 1 }) ⟶ Z} {b : Fin (n + 1) → (X.obj (Opposite.op { len := n }) ⟶ Z)}
  {a_1 : X.obj (Opposite.op { len := n + 1 }) ⟶ Z} {b_1 : Fin (n + 1) → (X.obj (Opposite.op { len := n }) ⟶ Z)},
  { a := a, b := b } = { a := a_1, b := b_1 } → a = a_1 ∧ b = b_1
-- Mathlib.CategoryTheory.Triangulated.Opposite.Triangle
CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso_inv_app_hom₃ : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  (X : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ),
  ((CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso C).inv.app X).hom₃ =
    CategoryTheory.CategoryStruct.id X.obj₃
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremConstraint.maxInsts.inj : ∀ {n n_1 : ℕ},
  Lean.Meta.Grind.EMatchTheoremConstraint.maxInsts n = Lean.Meta.Grind.EMatchTheoremConstraint.maxInsts n_1 → n = n_1
-- Lean.Compiler.IR.Basic
Lean.IR.Expr.fap.sizeOf_spec : ∀ (c : Lean.IR.FunId) (ys : Array Lean.IR.Arg), sizeOf (Lean.IR.Expr.fap c ys) = 1 + sizeOf c + sizeOf ys
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Neg
Std.Tactic.BVDecide.BVExpr.bitblast.blastNeg : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] → {w : ℕ} → (aig : Std.Sat.AIG α) → aig.RefVec w → Std.Sat.AIG.RefVecEntry α w
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_add_ofNat_mul' : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℕ) [inst_4 : m.AtLeastTwo],
  toIcoMod hp (a + OfNat.ofNat m * p) b = toIcoMod hp a b + OfNat.ofNat m * p
-- Mathlib.Order.BooleanAlgebra.Basic
compl_eq_top : ∀ {α : Type u} {x : α} [inst : BooleanAlgebra α], xᶜ = ⊤ ↔ x = ⊥
-- ImportGraph.Tools.FindHome
/-- Find locations as high as possible in the import hierarchy
where the named declaration could live.
Using `#find_home!` will forcefully remove the current file.
Note that this works best if used in a file with `import Mathlib`.

The current file could still be the only suggestion, even using `#find_home! lemma`.
The reason is that `#find_home!` scans the import graph below the current file,
selects all the files containing declarations appearing in `lemma`, excluding
the current file itself and looks for all least upper bounds of such files.

For a simple example, if `lemma` is in a file importing only `A.lean` and `B.lean` and
uses one lemma from each, then `#find_home! lemma` returns the current file.
 -/
«command#find_home!_» : Lean.ParserDescr
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.get?_diff_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∉ t₂ → (t₁ \ t₂).get? k = t₁.get? k
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapGrpFunctor_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : C ⥤ₗ D), CategoryTheory.Functor.mapGrpFunctor.obj F = F.obj.mapGrp
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.ConnectedComponent.mem_coe_supp_of_adj : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} {H : G.Subgraph} {c : H.coe.ConnectedComponent},
  v ∈ Subtype.val '' ↑c → w ∈ H.verts → H.Adj v w → w ∈ Subtype.val '' ↑c
-- Init.Core
beq_false_of_ne : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a b : α}, a ≠ b → (a == b) = false
-- Init.Data.String.Basic
String.Pos.Raw.isValidForSlice_prevAux : ∀ {s : String.Slice} (pos : s.Pos) (h : pos ≠ s.startPos), String.Pos.Raw.IsValidForSlice s (pos.prevAux h)
-- Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
UpperHalfPlane.prod_eq_zero_iff : ∀ {ι : Type u_1} {f : ι → UpperHalfPlane → ℂ} {s : Finset ι},
  (∀ i ∈ s, MDiff (f i)) → (∏ i ∈ s, f i = 0 ↔ ∃ i ∈ s, f i = 0)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- The map `embed v` is strictly monotone.  -/
ValuativeRel.ValueGroupWithZero.embed_strictMono : ∀ {R : Type u_2} {Γ : Type u_3} [inst : Ring R] [inst_1 : ValuativeRel R] [inst_2 : LinearOrderedCommGroupWithZero Γ]
  (v : Valuation R Γ) [inst_3 : v.Compatible], StrictMono ⇑(ValuativeRel.ValueGroupWithZero.embed v)
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Split.natTransCofanInj_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] {Δ : SimplexCategoryᵒᵖ}
  (A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ) (S : CategoryTheory.SimplicialObject.Split C),
  (CategoryTheory.SimplicialObject.Split.natTransCofanInj C A).app S = (S.s.cofan Δ).inj A
-- Lean.Meta.LazyDiscrTree
/-- Discrimination tree trie. See `LazyDiscrTree`.
 -/
Lean.Meta.LazyDiscrTree.Trie : Type → Type
-- Mathlib.Topology.Algebra.FilterBasis
/-- The topology associated to a module filter basis on a module over a topological ring.
It has the given basis as a basis of neighborhoods of zero. This version gets the ring
topology by unification instead of type class inference.  -/
ModuleFilterBasis.topology' : {R : Type u_3} →
  {M : Type u_4} →
    [inst : Semiring R] →
      {x : TopologicalSpace R} →
        [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → ModuleFilterBasis R M → TopologicalSpace M
-- Mathlib.CategoryTheory.Abelian.Images
/-- There is a canonical epimorphism `p : P ⟶ image f` for every `f`.  -/
CategoryTheory.Abelian.factorThruImage : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {P Q : C} →
        (f : P ⟶ Q) →
          [inst_2 : CategoryTheory.Limits.HasCokernel f] →
            [inst_3 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)] →
              P ⟶ CategoryTheory.Abelian.image f
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.Measure.setIntegral_toReal_rnDeriv' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ]
  [μ.HaveLebesgueDecomposition ν],
  μ.AbsolutelyContinuous ν → ∀ {s : Set α}, MeasurableSet s → ∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν = μ.real s
-- Mathlib.Analysis.Normed.Group.Basic
/-- A group homomorphism from a `Group` to a `SeminormedGroup` induces a `SeminormedGroup`
structure on the domain.  -/
SeminormedGroup.induced : {𝓕 : Type u_1} →
  (E : Type u_5) →
    (F : Type u_6) →
      [inst : FunLike 𝓕 E F] →
        [inst_1 : Group E] → [inst_2 : SeminormedGroup F] → [MonoidHomClass 𝓕 E F] → 𝓕 → SeminormedGroup E
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- A subgroup is closed under division.  -/
div_mem : ∀ {M : Type u_3} {S : Type u_4} [inst : DivInvMonoid M] [inst_1 : SetLike S M] [hSM : SubgroupClass S M] {H : S}
  {x y : M}, x ∈ H → y ∈ H → x / y ∈ H
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.currying_inverse_obj_map_app : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor (C × D) E) {X Y : C}
  (f : X ⟶ Y) (Y_1 : D),
  ((CategoryTheory.Functor.currying.inverse.obj F).map f).app Y_1 =
    F.map (CategoryTheory.Prod.mkHom f (CategoryTheory.CategoryStruct.id Y_1))
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.instAlgebraSubtypeMem_1 : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] →
          {S : IntermediateField K L} →
            {E : Type u_4} →
              [inst_3 : Field E] → [inst_4 : Algebra L E] → (T : IntermediateField (↥S) E) → Algebra ↥S ↥T
-- Lean.Declaration
Lean.ConstantInfo.defnInfo.injEq : ∀ (val val_1 : Lean.DefinitionVal), (Lean.ConstantInfo.defnInfo val = Lean.ConstantInfo.defnInfo val_1) = (val = val_1)
-- Mathlib.Combinatorics.SimpleGraph.DeleteEdges
SimpleGraph.deleteEdges.eq_1 : ∀ {V : Type u_1} (G : SimpleGraph V) (s : Set (Sym2 V)), G.deleteEdges s = G \ SimpleGraph.fromEdgeSet s
-- Init.Data.SInt.Lemmas
Int32.toInt_bmod_18446744073709551616 : ∀ (x : Int32), x.toInt.bmod 18446744073709551616 = x.toInt
-- Mathlib.NumberTheory.LSeries.HurwitzZetaValues
HurwitzZeta.hurwitzZetaEven_one_sub_two_mul_nat : ∀ {k : ℕ} {x : ℝ},
  k ≠ 0 →
    x ∈ Set.Icc 0 1 →
      HurwitzZeta.hurwitzZetaEven (↑x) (1 - 2 * ↑k) =
        -1 / (2 * ↑k) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided
CategoryTheory.MonoidalCategory.DayConvolution.braiding_naturality_right_assoc : ∀ {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.BraidedCategory C]
  [inst_4 : CategoryTheory.MonoidalCategory V] [inst_5 : CategoryTheory.BraidedCategory V]
  {F G : CategoryTheory.Functor C V} (H : CategoryTheory.Functor C V) (η : F ⟶ G)
  [inst_6 : CategoryTheory.MonoidalCategory.DayConvolution F H]
  [inst_7 : CategoryTheory.MonoidalCategory.DayConvolution H F]
  [inst_8 : CategoryTheory.MonoidalCategory.DayConvolution G H]
  [inst_9 : CategoryTheory.MonoidalCategory.DayConvolution H G] {Z : CategoryTheory.Functor C V}
  (h : CategoryTheory.MonoidalCategory.DayConvolution.convolution G H ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.DayConvolution.map (CategoryTheory.CategoryStruct.id H) η)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.braiding H G).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.braiding H F).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.DayConvolution.map η (CategoryTheory.CategoryStruct.id H)) h)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PushoutCocone.condition_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
  (t : CategoryTheory.Limits.PushoutCocone f g),
  t.ι.app CategoryTheory.Limits.WalkingSpan.zero = CategoryTheory.CategoryStruct.comp f t.inl
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.smul_apply' : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R] {M : Type u_7}
  [inst_2 : SMulZeroClass M R] (m : M) (s : HahnSeries.SummableFamily Γ R α) (a : α), (m • s) a = m • s a
-- Mathlib.Algebra.Group.Units.Equiv
MulEquiv.inv_symm : ∀ (G : Type u_6) [inst : DivisionCommMonoid G], (MulEquiv.inv G).symm = MulEquiv.inv G
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.univ_nontrivial : ∀ {α : Type u_1} [inst : Fintype α] [h : Nontrivial α], Finset.univ.Nontrivial
-- Mathlib.FieldTheory.Minpoly.Field
/-- If `y` is a conjugate of `x` over a field `K`, then it is a conjugate over a subring `R`.  -/
minpoly.aeval_of_isScalarTower : ∀ (R : Type u_3) {K : Type u_4} {T : Type u_5} {U : Type u_6} [inst : CommRing R] [inst_1 : Field K]
  [inst_2 : CommRing T] [inst_3 : Algebra R K] [inst_4 : Algebra K T] [inst_5 : Algebra R T] [IsScalarTower R K T]
  [inst_7 : CommSemiring U] [inst_8 : Algebra K U] [inst_9 : Algebra R U] [IsScalarTower R K U] (x : T) (y : U),
  (Polynomial.aeval y) (minpoly K x) = 0 → (Polynomial.aeval y) (minpoly R x) = 0
-- Init.Data.SInt.Lemmas
Int16.toBitVec_ofIntLE : ∀ (x : ℤ) (h₁ : Int16.minValue.toInt ≤ x) (h₂ : x ≤ Int16.maxValue.toInt),
  (Int16.ofIntLE x h₁ h₂).toBitVec = BitVec.ofInt 16 x
-- Mathlib.NumberTheory.NumberField.ClassNumber
NumberField.classNumber_pos : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K], 0 < NumberField.classNumber K
-- Mathlib.LinearAlgebra.QuadraticForm.Basis
QuadraticMap.toQuadraticMap_toBilin : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : LinearOrder ι] [inst_1 : CommRing R]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  (Q : QuadraticMap R M N) (bm : Module.Basis ι R M), (Q.toBilin bm).toQuadraticMap = Q
-- Mathlib.Order.Filter.Pointwise
Filter.div_le_div : ∀ {α : Type u_2} [inst : Div α] {f₁ f₂ g₁ g₂ : Filter α}, f₁ ≤ f₂ → g₁ ≤ g₂ → f₁ / g₁ ≤ f₂ / g₂
-- Mathlib.RingTheory.Valuation.ValuationRing
PreValuationRing.iff_ideal_total : ∀ {R : Type u_1} [inst : CommRing R], PreValuationRing R ↔ Std.Total fun x1 x2 => x1 ≤ x2
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.inclusion_inj : ∀ {M : Type u_1} [inst : AddZeroClass M] {S T : AddSubmonoid M} (h : S ≤ T) {x y : ↥S},
  (AddSubmonoid.inclusion h) x = (AddSubmonoid.inclusion h) y ↔ x = y
-- Mathlib.GroupTheory.Congruence.Opposite
Con.orderIsoOp_symm_apply : ∀ {M : Type u_1} [inst : Mul M] (c : Con Mᵐᵒᵖ), (RelIso.symm Con.orderIsoOp) c = c.unop
-- Mathlib.Algebra.Group.Defs
/-- A `DivisionMonoid` is a `DivInvMonoid` with involutive inversion and such that
`(a * b)⁻¹ = b⁻¹ * a⁻¹` and `a * b = 1 → a⁻¹ = b`.

This is the immediate common ancestor of `Group` and `GroupWithZero`.  -/
DivisionMonoid : Type u → Type u
-- Mathlib.Algebra.Category.HopfAlgCat.Basic
/-- A type alias for `BialgHom` to avoid confusion between the categorical and
algebraic spellings of composition.  -/
HopfAlgCat.Hom : {R : Type u} → [inst : CommRing R] → HopfAlgCat R → HopfAlgCat R → Type v
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.coe_mul : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Mul β] (f g : MeasureTheory.SimpleFunc α β),
  ⇑(f * g) = ⇑f * ⇑g
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.rnDeriv_eq_zero : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [μ.HaveLebesgueDecomposition ν],
  μ.rnDeriv ν =ᵐ[ν] 0 ↔ μ.MutuallySingular ν
-- Mathlib.Logic.Equiv.PartialEquiv
Equiv.toPartialEquivOfImageEq_target : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : Set α) (t : Set β) (h : ⇑e '' s = t),
  (e.toPartialEquivOfImageEq s t h).target = t
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.pi_zero : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] {ι : Type u_4} {φ : ι → Type u_5} [inst_4 : (i : ι) → TopologicalSpace (φ i)]
  [inst_5 : (i : ι) → AddCommMonoid (φ i)] [inst_6 : (i : ι) → Module R (φ i)], (ContinuousLinearMap.pi fun x => 0) = 0
-- Init.Data.Char.Lemmas
Char.leTrans : Trans (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
/-- `orthogonal` gives a `GaloisConnection` between
`ClosedSubmodule 𝕜 E` and its `OrderDual`.  -/
ClosedSubmodule.orthogonal_gc : ∀ (𝕜 : Type u_4) (E : Type u_5) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E],
  GaloisConnection ClosedSubmodule.orthogonal ClosedSubmodule.orthogonal
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.symm_bijective : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : Add β],
  Function.Bijective OrderAddMonoidIso.symm
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- If `2` is invertible in `R`, then applying the inverse of `2` in `End R M` to an element
of `M` is the same as multiplying by the inverse of `2` in `R`.  -/
QuadraticMap.half_moduleEnd_apply_eq_half_smul : ∀ {R : Type u_3} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Invertible 2] (x : M), ⅟2 x = ⅟2 • x
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHom.instBoundedLatticeHomClass : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : BoundedOrder α]
  [inst_3 : BoundedOrder β], BoundedLatticeHomClass (BoundedLatticeHom α β) α β
-- Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
WeierstrassCurve.ofJ_ne_0_ne_1728 : ∀ {F : Type u_2} [inst : Field F] (j : F) [inst_1 : DecidableEq F],
  j ≠ 0 → j ≠ 1728 → WeierstrassCurve.ofJ j = WeierstrassCurve.ofJNe0Or1728 j
-- Mathlib.Algebra.Group.Subsemigroup.Membership
Subsemigroup.mem_sup_left : ∀ {M : Type u_2} [inst : Mul M] {S T : Subsemigroup M} {x : M}, x ∈ S → x ∈ S ⊔ T
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.mkCoinductiveAux₂.congr_simp : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {P Q : CochainComplex V ℕ} (e : P ⟶ Q) (zero zero_1 : P.X 1 ⟶ Q.X 0) (e_zero : zero = zero_1)
  (comm_zero : e.f 0 = CategoryTheory.CategoryStruct.comp (P.d 0 1) zero) (one one_1 : P.X 2 ⟶ Q.X 1)
  (e_one : one = one_1)
  (comm_one :
    e.f 1 = CategoryTheory.CategoryStruct.comp zero (Q.d 0 1) + CategoryTheory.CategoryStruct.comp (P.d 1 2) one)
  (succ succ_1 :
    (n : ℕ) →
      (p :
          (f : P.X (n + 1) ⟶ Q.X n) ×'
            (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×'
              e.f (n + 1) =
                CategoryTheory.CategoryStruct.comp f (Q.d n (n + 1)) +
                  CategoryTheory.CategoryStruct.comp (P.d (n + 1) (n + 2)) f') →
        (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×'
          e.f (n + 2) =
            CategoryTheory.CategoryStruct.comp p.snd.fst (Q.d (n + 1) (n + 2)) +
              CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 3)) f''),
  succ = succ_1 →
    ∀ (n : ℕ),
      Homotopy.mkCoinductiveAux₂ e zero comm_zero one comm_one succ n =
        Homotopy.mkCoinductiveAux₂ e zero_1 ⋯ one_1 ⋯ succ_1 n
-- Init.Data.List.Find
List.findFinIdx?_eq_some_iff : ∀ {α : Type u_1} {xs : List α} {p : α → Bool} {i : Fin xs.length},
  List.findFinIdx? p xs = some i ↔ p xs[i] = true ∧ ∀ (j : Fin xs.length) (hji : j < i), ¬p xs[j] = true
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.sum_tensor : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {P Q R S : C} {J : Type u_2}
  (s : Finset J) (f : P ⟶ Q) (g : J → (R ⟶ S)),
  CategoryTheory.MonoidalCategoryStruct.tensorHom (∑ j ∈ s, g j) f =
    ∑ j ∈ s, CategoryTheory.MonoidalCategoryStruct.tensorHom (g j) f
-- Mathlib.RingTheory.LocalRing.ResidueField.Polynomial
/-- Given a prime `P` of `R` and an ideal `I` of `R[X]`, the image of `I` in `κ(P)[X]`
is generated by some `p ∈ I` (basically because `κ(P)[X]` is a PID).  -/
Ideal.exists_mem_span_singleton_map_residueField_eq : ∀ {R : Type u_1} [inst : CommRing R] (P : Ideal R) [inst_1 : P.IsPrime] (I : Ideal (Polynomial R)),
  ∃ p ∈ I,
    Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p} =
      Ideal.map (Polynomial.mapRingHom (algebraMap R P.ResidueField)) I
-- Mathlib.RingTheory.Congruence.Defs
/-- Extensionality rule for congruence relations.  -/
RingCon.ext : ∀ {R : Type u_1} [inst : Add R] [inst_1 : Mul R] {c d : RingCon R}, (∀ (x y : R), c x y ↔ d x y) → c = d
-- Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
HomotopicalAlgebra.CofibrantBrownFactorization.mk'_i : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : HomotopicalAlgebra.IsCofibrant X] [inst_3 : HomotopicalAlgebra.IsCofibrant Y]
  (h :
    (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C)
      (CategoryTheory.Limits.coprod.desc f (CategoryTheory.CategoryStruct.id Y))),
  (HomotopicalAlgebra.CofibrantBrownFactorization.mk' f h).i =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl h.i
-- Mathlib.MeasureTheory.Measure.Haar.Basic
/-- The variant of `addCHaar_self` for `addHaarContent`.  -/
MeasureTheory.Measure.haar.addHaarContent_self : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G]
  {K₀ : TopologicalSpace.PositiveCompacts G}, (MeasureTheory.Measure.haar.addHaarContent K₀) K₀.toCompacts = 1
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.PositiveCompacts.ext : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s t : TopologicalSpace.PositiveCompacts α}, ↑s = ↑t → s = t
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.equiv_iff_keysArray_unit_perm : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α (fun x => Unit) cmp},
  t₁.Equiv t₂ ↔ t₁.keysArray.Perm t₂.keysArray
-- Mathlib.Data.NNRat.Defs
/-- Coercion `ℚ≥0 → ℚ` as a `RingHom`.  -/
NNRat.coeHom : ℚ≥0 →+* ℚ
-- Mathlib.Algebra.Order.Archimedean.Basic
existsUnique_add_zsmul_mem_Ioc : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] {a : G},
  0 < a → ∀ (b c : G), ∃! m, b + m • a ∈ Set.Ioc c (c + a)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.unitOfList_singleton : ∀ {α : Type u} {cmp : α → α → Ordering} {k : α}, Std.DTreeMap.Raw.Const.unitOfList [k] cmp = ∅.insertIfNew k ()
-- Mathlib.Combinatorics.Matroid.Minor.Delete
Matroid.delete_isBase_iff : ∀ {α : Type u_1} {M : Matroid α} {B D : Set α}, (M.delete D).IsBase B ↔ M.IsBasis B (M.E \ D)