mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.newton_seq_dist_to_a : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F : Polynomial R} {a : ℤ_[p]}
  (hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2),
  (Polynomial.aeval a) F ≠ 0 →
    ∀ (n : ℕ),
      0 < n →
        ‖newton_seq_gen✝ hnorm n - a‖ = ‖(Polynomial.aeval a) F‖ / ‖(Polynomial.aeval a) (Polynomial.derivative F)‖
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- Second projection from the intersection of two pre-`0`-hypercovers.  -/
CategoryTheory.PreZeroHypercover.interSnd : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      (E : CategoryTheory.PreZeroHypercover S) →
        (F : CategoryTheory.PreZeroHypercover S) →
          [inst_1 : ∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] → (E.inter F).Hom F
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.T_sub_two : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ),
  Polynomial.Chebyshev.T R (n - 2) = 2 * Polynomial.X * Polynomial.Chebyshev.T R (n - 1) - Polynomial.Chebyshev.T R n
-- Mathlib.RingTheory.Kaehler.Basic
Algebra.EssFiniteType.finset.congr_simp : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [h : Algebra.EssFiniteType R S], Algebra.EssFiniteType.finset R S = Algebra.EssFiniteType.finset R S
-- Lean.Elab.PreDefinition.Basic
Lean.Elab.addAndCompilePartialRec : Lean.LocalContext × Lean.LocalInstances → Array Lean.Elab.PreDefinition → Lean.Elab.TermElabM Unit
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.coeff_monomial_mul' : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (m s : σ →₀ ℕ) (r : R) (p : MvPolynomial σ R),
  MvPolynomial.coeff m ((MvPolynomial.monomial s) r * p) = if s ≤ m then r * MvPolynomial.coeff (m - s) p else 0
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mfderivWithin_const : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {s : Set M} {x : M} {c : M'},
  (mfderiv[s] fun x => c) x = 0
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.pentagon_inv_hom_hom_hom_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {W X Y Z : C},
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj W X) Y Z).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.associator W X Y).hom
          Z)
        (CategoryTheory.MonoidalCategoryStruct.associator W (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
            Z).hom) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator W X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).hom
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv)
-- ProofWidgets.Presentation.Expr
ProofWidgets.ExprPresentations.mk : Array ProofWidgets.ExprPresentationData → ProofWidgets.ExprPresentations
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.LaxRightLinear.μᵣ_associativity_inv : ∀ {D : Type u_1} {D' : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} D]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D'] (F : CategoryTheory.Functor D D') {C : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C] [inst_3 : CategoryTheory.MonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D]
  [inst_5 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D'] [inst_6 : F.LaxRightLinear C] (d : D) (c c' : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft
        (CategoryTheory.Functor.LaxRightLinear.μᵣ F d c) c')
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.LaxRightLinear.μᵣ F
          (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c) c')
        (F.map (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c c').inv)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso (F.obj d) c c').inv
      (CategoryTheory.Functor.LaxRightLinear.μᵣ F d (CategoryTheory.MonoidalCategoryStruct.tensorObj c c'))
-- Mathlib.Order.Hom.Set
StrictMono.coe_orderIsoOfSurjective : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Preorder β] (f : α → β) (h_mono : StrictMono f)
  (h_surj : Function.Surjective f), ⇑(StrictMono.orderIsoOfSurjective f h_mono h_surj) = f
-- Mathlib.Analysis.Normed.Field.Lemmas
Filter.map_mul_left_cobounded : ∀ {α : Type u_1} [inst : NormedDivisionRing α] {a : α},
  a ≠ 0 → Filter.map (fun x => a * x) (Bornology.cobounded α) = Bornology.cobounded α
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
/-- A variant of `WeierstrassCurve.j_eq_zero_iff_of_char_two` without assuming a reduced ring.  -/
WeierstrassCurve.j_eq_zero_iff_of_char_two' : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [inst_1 : W.IsElliptic] [CharP R 2], W.j = 0 ↔ W.a₁ ^ 12 = 0
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_hom_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] {F G : CategoryTheory.Pseudofunctor B CategoryTheory.Cat}
  (α : F ⟶ G) {a b : B} {f g : a ⟶ b} (η : f ≅ g) (X : ↑(F.obj a)) {Z : ↑(G.obj b)}
  (h : (G.map g).toFunctor.obj ((α.app a).toFunctor.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((α.naturality g).hom.toNatTrans.app X) h =
    CategoryTheory.CategoryStruct.comp ((α.app b).toFunctor.map ((F.map₂ η.inv).toNatTrans.app X))
      (CategoryTheory.CategoryStruct.comp ((α.naturality f).hom.toNatTrans.app X)
        (CategoryTheory.CategoryStruct.comp ((G.map₂ η.hom).toNatTrans.app ((α.app a).toFunctor.obj X)) h))
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.coeIdeal_finprod : ∀ {R : Type u_1} [inst : CommRing R] (S : Submonoid R) (P : Type u_2) [inst_1 : CommRing P] [inst_2 : Algebra R P]
  [IsLocalization S P] {α : Sort u_3} {f : α → Ideal R}, S ≤ nonZeroDivisors R → ↑(∏ᶠ (a : α), f a) = ∏ᶠ (a : α), ↑(f a)
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.instHasImageHomMk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f],
  CategoryTheory.Limits.HasImage (CategoryTheory.Arrow.mk f).hom
-- Mathlib.Logic.Unique
Unique.subtypeEq' : {α : Sort u_1} → (y : α) → Unique { x // y = x }
-- Mathlib.Algebra.Group.Submonoid.Units
Subgroup.unit_of_mem_ofUnits_spec_eq_of_val_mem : ∀ {M : Type u_1} [inst : Monoid M] (S : Subgroup Mˣ) {x : Mˣ} (h : ↑x ∈ S.ofUnits), S.unit_of_mem_ofUnits h = x
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.braiding_inv_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y : C) {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (β_ X Y).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst Y X) h
-- Init.Core
/-- A helper gadget for instructing the kernel to eagerly reduce terms.

When the gadget wraps the argument of an application, then when checking that
the expected and inferred type of the argument match, the kernel will evaluate terms more eagerly.
It is often used to wrap `Eq.refl true` proof terms as `eagerReduce (Eq.refl true)`
when using proof by reflection.
As an example, consider the theorem:
```
theorem eq_norm (ctx : Context) (p₁ p₂ : Poly) (h : (p₁.norm == p₂) = true) :
  p₁.denote ctx = 0 → p₂.denote ctx = 0
```
The argument `h : (p₁.norm == p₂) = true` is a candidate for `eagerReduce`.
When applying this theorem, we would write:

```
eq_norm ctx p q (eagerReduce (Eq.refl true)) h
```
to instruct the kernel to use eager reduction when establishing that `(p.norm == q) = true` is
definitionally equal to `true = true`.
 -/
eagerReduce : {α : Sort u} → α → α
-- Init.Data.Vector.Lemmas
Vector.getElem_set!_self : ∀ {α : Type u_1} {n i : ℕ} {xs : Vector α n} {x : α} (hi : i < n), (xs.set! i x)[i] = x
-- Mathlib.Algebra.Lie.Derivation.BaseChange
Lie.Derivation.ofDerivation_apply : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra R A] {L : Type u_3}
  [inst_3 : LieRing L] [inst_4 : LieAlgebra R L] (d : Derivation R A A) (x : TensorProduct R A L),
  ((Lie.Derivation.ofDerivation L) d) x = (LinearMap.rTensor L ↑d) x
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.piEquivPiSubtypeProd_symm_apply : ∀ {ι : Type u_7} (p : ι → Prop) [inst : DecidablePred p] (Y : ι → Type u_8)
  [inst_1 : (i : ι) → NonUnitalNonAssocSemiring (Y i)] (f : ((i : { x // p x }) → Y ↑i) × ((i : { x // ¬p x }) → Y ↑i))
  (x : ι), (RingEquiv.piEquivPiSubtypeProd p Y).symm f x = if h : p x then f.1 ⟨x, h⟩ else f.2 ⟨x, h⟩
-- Mathlib.Analysis.Normed.Operator.Mul
/-- The left regular representation of the algebra on itself is an isometry.  -/
RegularNormedAlgebra.isometry_mul' : ∀ {𝕜 : Type u_1} {inst : NontriviallyNormedField 𝕜} {R : Type u_3} {inst_1 : NonUnitalSeminormedRing R}
  {inst_2 : NormedSpace 𝕜 R} {inst_3 : IsScalarTower 𝕜 R R} {inst_4 : SMulCommClass 𝕜 R R}
  [self : RegularNormedAlgebra 𝕜 R], Isometry ⇑(ContinuousLinearMap.mul 𝕜 R)
-- Mathlib.RingTheory.Algebraic.Basic
IsAlgebraic.of_aeval : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {r : A} (f : Polynomial R),
  f.natDegree ≠ 0 → f.leadingCoeff ∈ nonZeroDivisors R → IsAlgebraic R ((Polynomial.aeval r) f) → IsAlgebraic R r
-- Mathlib.NumberTheory.FLT.Three
/-- Given `(S : Solution)`, we have that `λ ∣ (S.a + η ^ 2 * S.b)`.  -/
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.lambda_dvd_a_add_eta_sq_mul_b : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : FermatLastTheoremForThreeGen.Solution✝ hζ),
  hζ.toInteger - 1 ∣
    FermatLastTheoremForThreeGen.Solution'.a✝ (FermatLastTheoremForThreeGen.Solution.toSolution'✝ S) +
      ↑⋯.unit ^ 2 * FermatLastTheoremForThreeGen.Solution'.b✝ (FermatLastTheoremForThreeGen.Solution.toSolution'✝ S)
-- Init.Data.String.Lemmas.FindPos
String.Pos.prev?_toSlice : ∀ {s : String} {p : s.Pos}, p.toSlice.prev? = Option.map String.Pos.toSlice p.prev?
-- Lean.Elab.PreDefinition.TerminationMeasure
Lean.Elab.TerminationMeasure.mk : Lean.Syntax → Bool → Lean.Expr → Lean.Elab.TerminationMeasure
-- Mathlib.Algebra.Order.Interval.Multiset
Multiset.map_add_left_Ioc : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α]
  [inst_4 : LocallyFiniteOrder α] (a b c : α),
  Multiset.map (fun x => c + x) (Multiset.Ioc a b) = Multiset.Ioc (c + a) (c + b)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
/-- If the coproduct comparison maps of `G` at every pair `(X,Y)` is an
isomorphism, then `G` preserves binary coproducts.  -/
CategoryTheory.Limits.preservesBinaryCoproducts_of_isIso_coprodComparison : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C]
  [inst_3 : CategoryTheory.Limits.HasBinaryCoproducts D]
  [i : ∀ {X Y : C}, CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison G X Y)],
  CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) G
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjId_hom_app_fst_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] (X_1 : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X)
  (X_2 : X),
  ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjId F G X).hom.app X_1).fst.app X_2 =
    CategoryTheory.CategoryStruct.id (X_1.fst.obj X_2)
-- Lean.Parser.Term.Basic
Lean.Parser.Tactic.sepBy1IndentSemicolon.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.getD_diff_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {k fallback : α},
  k ∉ t₁ → (t₁ \ t₂).getD k fallback = fallback
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.mk.congr_simp : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] {𝒜 : ℕ → σ}
  [inst_3 : GradedRing 𝒜] (asHomogeneousIdeal asHomogeneousIdeal_1 : HomogeneousIdeal 𝒜)
  (e_asHomogeneousIdeal : asHomogeneousIdeal = asHomogeneousIdeal_1) (isPrime : asHomogeneousIdeal.toIdeal.IsPrime)
  (not_irrelevant_le : ¬HomogeneousIdeal.irrelevant 𝒜 ≤ asHomogeneousIdeal),
  { asHomogeneousIdeal := asHomogeneousIdeal, isPrime := isPrime, not_irrelevant_le := not_irrelevant_le } =
    { asHomogeneousIdeal := asHomogeneousIdeal_1, isPrime := ⋯, not_irrelevant_le := ⋯ }
-- Mathlib.Logic.IsEmpty.Basic
biTotal_iff_isEmpty_left : ∀ {α : Type u_4} {β : Type u_5} (R : α → β → Prop) [IsEmpty β], Relator.BiTotal R ↔ IsEmpty α
-- Lean.DocString.Parser
/-- The minimum indentation of a continuation line for the current paragraph
 -/
Lean.Doc.Parser.InlineCtxt.minIndent : Lean.Doc.Parser.InlineCtxt → ℕ
-- Mathlib.Algebra.Group.Basic
boole_nsmul : ∀ {M : Type u_4} [inst : AddMonoid M] (P : Prop) [inst_1 : Decidable P] (a : M),
  (if P then 1 else 0) • a = if P then a else 0
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ContinuousHom.mk.injEq : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β]
  (toOrderHom : α →o β)
  (map_ωSup' :
    ∀ (c : OmegaCompletePartialOrder.Chain α),
      toOrderHom.toFun (OmegaCompletePartialOrder.ωSup c) = OmegaCompletePartialOrder.ωSup (c.map toOrderHom))
  (toOrderHom_1 : α →o β)
  (map_ωSup'_1 :
    ∀ (c : OmegaCompletePartialOrder.Chain α),
      toOrderHom_1.toFun (OmegaCompletePartialOrder.ωSup c) = OmegaCompletePartialOrder.ωSup (c.map toOrderHom_1)),
  ({ toOrderHom := toOrderHom, map_ωSup' := map_ωSup' } = { toOrderHom := toOrderHom_1, map_ωSup' := map_ωSup'_1 }) =
    (toOrderHom = toOrderHom_1)
-- Mathlib.Data.Matrix.Mul
/-- Permuting a vector on the left of a dot product can be transferred to the right.  -/
comp_equiv_symm_dotProduct : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : NonUnitalNonAssocSemiring α] (u : m → α) (x : n → α) (e : m ≃ n), u ∘ ⇑e.symm ⬝ᵥ x = u ⬝ᵥ x ∘ ⇑e
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKey_modify_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] [Inhabited α] {k : α} {f : β → β} {h : k ∈ Std.DHashMap.Const.modify m k f},
  (Std.DHashMap.Const.modify m k f).getKey k h = k
-- Mathlib.CategoryTheory.Adjunction.Lifting.Right
/-- The adjoint triangle theorem: Suppose `U : A ⥤ B` has a left adjoint `F` such that each unit
`η_X : X ⟶ UFX` is a regular monomorphism. Then if a category `C` has equalizers of coreflexive
pairs, then a functor `L : C ⥤ B` has a right adjoint if the composite `L ⋙ F` does.

Note the converse is true (with weaker assumptions), by `Adjunction.comp`.
See https://ncatlab.org/nlab/show/adjoint+triangle+theorem
 -/
CategoryTheory.isLeftAdjoint_triangle_lift : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {U : CategoryTheory.Functor A B} {F : CategoryTheory.Functor B A} (L : CategoryTheory.Functor C B) (adj₁ : F ⊣ U)
  (h : (X : B) → CategoryTheory.RegularMono (adj₁.unit.app X)) [CategoryTheory.Limits.HasCoreflexiveEqualizers C]
  [(L.comp F).IsLeftAdjoint], L.IsLeftAdjoint
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get?_eq_some_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t.WF → ∀ {k : α} {v : β k}, t.get? k = some v ↔ ∃ (h : k ∈ t), t.get k h = v
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
QuotientAddGroup.measurableSpace : {G : Type u_6} → [inst : AddGroup G] → [MeasurableSpace G] → (S : AddSubgroup G) → MeasurableSpace (G ⧸ S)
-- Mathlib.Data.QPF.Multivariate.Constructions.Cofix
/-- Bisimulation principle using `LiftR'` to match and relate children of two trees.  -/
MvQPF.Cofix.bisim₂ : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n}
  (r : MvQPF.Cofix F α → MvQPF.Cofix F α → Prop),
  (∀ (x y : MvQPF.Cofix F α), r x y → MvFunctor.LiftR' (α.RelLast' r) x.dest y.dest) →
    ∀ (x y : MvQPF.Cofix F α), r x y → x = y
-- Mathlib.Topology.Connected.PathConnected
isPathConnected_iff_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] {F : Set X}, IsPathConnected F ↔ ∃ x ∈ F, pathComponentIn F x = F
-- Mathlib.Computability.ContextFreeGrammar
/-- **Alias** of the reverse direction of `ContextFreeGrammar.produces_reverse`. -/
ContextFreeGrammar.Produces.reverse : ∀ {T : Type u_1} {g : ContextFreeGrammar T} {u v : List (Symbol T g.NT)},
  g.Produces u v → g.reverse.Produces u.reverse v.reverse
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.CoordinateRing.norm_smul_basis : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} (p q : Polynomial R),
  (Algebra.norm (Polynomial R)) (p • 1 + q • (WeierstrassCurve.Affine.CoordinateRing.mk W') Polynomial.X) =
    p ^ 2 - p * q * (Polynomial.C W'.a₁ * Polynomial.X + Polynomial.C W'.a₃) -
      q ^ 2 *
        (Polynomial.X ^ 3 + Polynomial.C W'.a₂ * Polynomial.X ^ 2 + Polynomial.C W'.a₄ * Polynomial.X +
          Polynomial.C W'.a₆)
-- Mathlib.Analysis.Normed.Operator.Prod
/-- The operator norm of the second projection `E × F → F` is exactly 1 if `F` is nontrivial.  -/
ContinuousLinearMap.norm_snd : ∀ (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [Nontrivial F],
  ‖ContinuousLinearMap.snd 𝕜 E F‖ = 1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PushoutCocone.mk_ι_app_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {W : C} (inl : Y ⟶ W)
  (inr : Z ⟶ W) (eq : CategoryTheory.CategoryStruct.comp f inl = CategoryTheory.CategoryStruct.comp g inr),
  (CategoryTheory.Limits.PushoutCocone.mk inl inr eq).ι.app CategoryTheory.Limits.WalkingSpan.zero =
    CategoryTheory.CategoryStruct.comp f inl
-- Mathlib.Data.Real.Basic
Real.mk_lt : ∀ {f g : CauSeq ℚ abs}, Real.mk f < Real.mk g ↔ f < g
-- Mathlib.NumberTheory.Zsqrtd.GaussianInt
GaussianInt.div_def : ∀ (x y : GaussianInt),
  x / y = { re := round (↑(x * star y).re / ↑(Zsqrtd.norm y)), im := round (↑(x * star y).im / ↑(Zsqrtd.norm y)) }
-- Init.Data.Stream
Stream.next? : {stream : Type u} → {value : outParam (Type v)} → [self : Std.Stream stream value] → stream → Option (value × stream)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PullbackObjObj.ofHasPullback_snd : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  (G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₃ Y₃ : C₃}
  (f₃ : X₃ ⟶ Y₃) [inst_3 : CategoryTheory.Limits.HasPullback ((G.obj (Opposite.op X₁)).map f₃) ((G.map f₁.op).app Y₃)],
  (CategoryTheory.Functor.PullbackObjObj.ofHasPullback G f₁ f₃).snd =
    CategoryTheory.Limits.pullback.snd ((G.obj (Opposite.op X₁)).map f₃) ((G.map f₁.op).app Y₃)
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.BifunctorComp₁₂IndexData.hpq : ∀ {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J}
  (self : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r) (i : I₁ × I₂ × I₃),
  self.q (self.p (i.1, i.2.1), i.2.2) = r i
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
IsDiscreteValuationRing.coheight_pow_maximalIdeal : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] (n : ℕ),
  Order.coheight (IsLocalRing.maximalIdeal R ^ n) = ↑n
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineSubspace.toContinuousAffineMap_subtypeₐᵢ : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P] (s : AffineSubspace 𝕜 P)
  [inst_5 : Nonempty ↥s], s.subtypeₐᵢ.toContinuousAffineMap = s.subtypeA
-- Init.Data.List.MinMax
List.max_cons_cons : ∀ {α : Type u_1} [inst : Max α] {a b : α} {l : List α}, (a :: b :: l).max ⋯ = (a ⊔ b :: l).max ⋯
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.invVeblen₂_zero : Ordinal.invVeblen₂ 0 = 0
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.nsmul_univ : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddMonoid α] {n : ℕ} [inst_2 : Fintype α],
  n ≠ 0 → n • Finset.univ = Finset.univ
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.coe_map : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] [inst_6 : Semiring B] [inst_7 : StarRing B]
  [inst_8 : Algebra R B] [inst_9 : StarModule R B] (S : StarSubalgebra R A) (f : A →⋆ₐ[R] B),
  ↑(StarSubalgebra.map f S) = ⇑f '' ↑S
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.IsCycleOn.zpow_apply_eq : ∀ {α : Type u_2} {f : Equiv.Perm α} {a : α} {s : Finset α},
  f.IsCycleOn ↑s → a ∈ s → ∀ {n : ℤ}, (f ^ n) a = a ↔ ↑s.card ∣ n
-- Mathlib.Topology.Algebra.Nonarchimedean.Basic
/-- The Cartesian product of two nonarchimedean rings is nonarchimedean.  -/
NonarchimedeanRing.instProd : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : TopologicalSpace R] [NonarchimedeanRing R] [inst_3 : Ring S]
  [inst_4 : TopologicalSpace S] [NonarchimedeanRing S], NonarchimedeanRing (R × S)
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
CategoryTheory.Lax.LaxTrans.homCategory_comp_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} {X Y Z : F ⟶ G} (Γ : CategoryTheory.Lax.LaxTrans.Hom X Y)
  (Δ : CategoryTheory.Lax.LaxTrans.Hom Y Z) (a : B),
  (CategoryTheory.CategoryStruct.comp Γ Δ).as.app a = CategoryTheory.CategoryStruct.comp (Γ.as.app a) (Δ.as.app a)
-- Mathlib.CategoryTheory.NatTrans
/-- `NatTrans F G` represents a natural transformation between functors `F` and `G`.

The field `app` provides the components of the natural transformation.

Naturality is expressed by `α.naturality`.
 -/
CategoryTheory.NatTrans : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.Functor C D → CategoryTheory.Functor C D → Type (max u₁ v₂)