mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Control.Lawful.Instances
ExceptT.tryCatch.eq_1 : ∀ {ε : Type u} {m : Type u → Type v} [inst : Monad m] {α : Type u} (ma : ExceptT ε m α) (handle : ε → ExceptT ε m α),
  ma.tryCatch handle =
    ExceptT.mk do
      let res ← ma
      match res with
        | Except.ok a => pure (Except.ok a)
        | Except.error e => handle e
-- Mathlib.Topology.Algebra.InfiniteSum.Order
Finite.of_summable_const : ∀ {ι : Type u_1} {α : Type u_3} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α]
  [inst_3 : TopologicalSpace α] [Archimedean α] [OrderClosedTopology α] {b : α},
  0 < b → (Summable fun x => b) → Finite ι
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
/-- Equivalence between a `TensorProduct` of `PiTensorProduct`s and a single
`PiTensorProduct` indexed by a `Sum` type.

See `PiTensorProduct.tmulEquivDep` for the dependent version.  -/
PiTensorProduct.tmulEquiv : {ι : Type u_1} →
  {ι₂ : Type u_2} →
    (R : Type u_4) →
      [inst : CommSemiring R] →
        (M : Type u_8) →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Module R M] →
              TensorProduct R (PiTensorProduct R fun x => M) (PiTensorProduct R fun x => M) ≃ₗ[R]
                PiTensorProduct R fun x => M
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_mul_const_Iio_of_neg : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (a : α) {c : α},
  c < 0 → (fun x => x * c) ⁻¹' Set.Iio a = Set.Ioi (a / c)
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.frequently_mul_le : ∀ {u : ℕ → EReal} {a : EReal}, a < LinearGrowth.linearGrowthSup u → ∃ᶠ (n : ℕ) in Filter.atTop, a * ↑n ≤ u n
-- Mathlib.Analysis.SpecialFunctions.Log.Deriv
derivWithin.log : ∀ {f : ℝ → ℝ} {x : ℝ} {s : Set ℝ},
  DifferentiableWithinAt ℝ f s x →
    f x ≠ 0 → UniqueDiffWithinAt ℝ s x → derivWithin (fun x => Real.log (f x)) s x = derivWithin f s x / f x
-- Mathlib.Data.Finmap
Finset.erase.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α) (a : α), s.erase a = { val := s.val.erase a, nodup := ⋯ }
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
/-- `rpowIntegrand₀₁ p t` is operator concave for all `p ∈ Ioo 0 1`  -/
CFC.concaveOn_cfc_rpowIntegrand₀₁ : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {p t : ℝ},
  p ∈ Set.Ioo 0 1 → 0 < t → ConcaveOn ℝ (Set.Ici 0) (cfc (p.rpowIntegrand₀₁ t))
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.hom_id : ∀ {R : Type u} [inst : Semiring R] {M : SemimoduleCat R},
  SemimoduleCat.Hom.hom (CategoryTheory.CategoryStruct.id M) = LinearMap.id
-- Mathlib.Algebra.MonoidAlgebra.Grading
AddMonoidAlgebra.gradeBy.gradedMonoid : ∀ {M : Type u_1} {ι : Type u_2} {R : Type u_3} [inst : AddMonoid M] [inst_1 : AddMonoid ι] [inst_2 : CommSemiring R]
  (f : M →+ ι), SetLike.GradedMonoid (AddMonoidAlgebra.gradeBy R ⇑f)
-- Mathlib.MeasureTheory.Measure.Portmanteau
/-- One implication of the portmanteau theorem: if for all open sets `G` we have the liminf
condition `μ(G) ≤ liminf μsₙ(G)`, then the measures `μsₙ` converge weakly to the measure `μ`.

This lemma uses a coercion from `ProbabilityMeasure` to `Measure` in the hypothesis.
See `tendsto_of_forall_isOpen_le_liminf` for the version without coercion.  -/
MeasureTheory.tendsto_of_forall_isOpen_le_liminf' : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
  {ι : Type u_2} {μ : MeasureTheory.ProbabilityMeasure Ω} {μs : ι → MeasureTheory.ProbabilityMeasure Ω} {L : Filter ι}
  [L.IsCountablyGenerated],
  (∀ (G : Set Ω), IsOpen G → ↑μ G ≤ Filter.liminf (fun i => ↑(μs i) G) L) → Filter.Tendsto (fun i => μs i) L (nhds μ)
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
/-- `f` is continuously differentiable at each point outside of its `mulTSupport`.  -/
contMDiffAt_of_notMem_mulTSupport : ∀ {𝕜 : 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] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_7 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7}
  [inst_8 : TopologicalSpace M'] [inst_9 : ChartedSpace H M] [inst_10 : ChartedSpace H' M'] {f : M → M'}
  [inst_11 : One M'] {x : M}, x ∉ mulTSupport f → ∀ (n : WithTop ℕ∞), ContMDiffAt I I' n f x
-- Mathlib.Data.EReal.Inv
EReal.exists_nat_ge_mul : ∀ {a : EReal}, a ≠ ⊤ → ∀ (n : ℕ), ∃ m, a * ↑n ≤ ↑m
-- Mathlib.Data.Set.Basic
Set.eq_empty_of_isEmpty : ∀ {α : Type u} (s : Set α) [IsEmpty ↑s], s = ∅
-- Mathlib.Order.Filter.Ultrafilter.Basic
Filter.bot_ne_hyperfilter : ∀ {α : Type u} [inst : Infinite α], ⊥ ≠ ↑(Filter.hyperfilter α)
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.transvection_mul_apply_same : ∀ {n : Type u_1} {R : Type u₂} [inst : DecidableEq n] [inst_1 : CommRing R] (i j : n) [inst_2 : Fintype n]
  {m : Type u_4} (b : m) (c : R) (M : Matrix n m R), (Matrix.transvection i j c * M) i b = M i b + c * M j b
-- Batteries.Data.List.Basic
List.takeD.eq_2 : ∀ {α : Type u_1} (x : List α) (x_1 : α) (n : ℕ), List.takeD n.succ x x_1 = x.headD x_1 :: List.takeD n x.tail x_1
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
/-- A homotopy equivalence between two short complexes `S₁` and `S₂` consists
of morphisms `hom : S₁ ⟶ S₂` and `inv : S₂ ⟶ S₁` such that both compositions
`hom ≫ inv` and `inv ≫ hom` are homotopic to the identity.  -/
CategoryTheory.ShortComplex.HomotopyEquiv : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] → CategoryTheory.ShortComplex C → CategoryTheory.ShortComplex C → Type v_1
-- Lean.Setup
Lean.ImportArtifacts.ir? : Lean.ImportArtifacts → Option System.FilePath
-- Init.Data.String.Lemmas.Iterate
String.Model.positionsFrom_eq_map : ∀ {s : String} {p : s.Pos},
  String.Model.positionsFrom p =
    List.map (fun p => ⟨String.Pos.ofToSlice ↑p, ⋯⟩) (String.Slice.Model.positionsFrom p.toSlice)
-- Mathlib.Data.LawfulXor.Basic
instLawfulXorISize : LawfulXor ISize
-- Init.Prelude
MonadStateOf.mk : {σ : semiOutParam (Type u)} →
  {m : Type u → Type v} → m σ → (σ → m PUnit.{u + 1}) → ({α : Type u} → (σ → α × σ) → m α) → MonadStateOf σ m
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.eq_zero_of_forall_eval_zero_of_natDegree_lt_card : ∀ {R : Type u} [inst : CommRing R] [IsDomain R] (f : Polynomial R),
  (∀ (r : R), Polynomial.eval r f = 0) → ↑f.natDegree < Cardinal.mk R → f = 0
-- Mathlib.Tactic.ClickSuggestions.Util
/-- If the set of computations is non-empty, display a `⏳️` symbol with hover information that
shows all of the ongoing computations.  -/
_private.Mathlib.Tactic.ClickSuggestions.Util.0.Mathlib.Tactic.ClickSuggestions.trackingComputation.renderStatus : Mathlib.Tactic.ClickSuggestions.ClickSuggestionsM Unit
-- Mathlib.Order.Interval.Set.Infinite
Set.instInfiniteElemIciOfNoMaxOrder : ∀ {α : Type u_1} [inst : Preorder α] [NoMaxOrder α] {a : α}, Infinite ↑(Set.Ici a)
-- Std.Do.PredTrans
/-- Apply the predicate transformer to a postcondition.
 -/
Std.Do.PredTrans.apply : {ps : Std.Do.PostShape} → {α : Type u} → Std.Do.PredTrans ps α → Std.Do.PostCond α ps → Std.Do.Assertion ps
-- Mathlib.RepresentationTheory.Homological.FiniteCyclic
/-- Given a finite cyclic group `G` generated by `g : G` and a `k`-linear `G`-representation `A`,
this is the periodic chain complex in `ModuleCat k` given by
`... ⟶ A --N--> A --(ρ(g) - 𝟙)--> A --N--> A --(ρ(g) - 𝟙)--> A ⟶ 0` where `N` is the norm map.
Its homology is the group homology of `A`.  -/
Rep.FiniteCyclicGroup.moduleCatChainComplex : {k G : Type u} →
  [inst : CommRing k] → [inst_1 : CommGroup G] → [Fintype G] → Rep.{u_1, u, u} k G → G → ChainComplex (ModuleCat k) ℕ
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.ofAlgEquiv_apply : ∀ {S : Type u_5} [inst : CommRing S] (I : Ideal S) [inst_1 : IsAdicComplete I S] (x : S),
  (AdicCompletion.ofAlgEquiv I) x = (AdicCompletion.of I S) x
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
SummationFilter.instLeAtTopOfIsEmpty : ∀ {β : Type u_2} [IsEmpty β] (L : SummationFilter β), L.LeAtTop
-- Mathlib.Data.ENat.Basic
/-- **Alias** of `ENat.natCast_add_one_le_iff`. -/
ENat.coe_add_one_le_iff : ∀ {m : ℕ} {n : ℕ∞}, ↑m + 1 ≤ n ↔ ↑m < n
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.ae_eq_set_sdiff : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} {s t s' t' : Set α}, s =ᵐ[μ] t → s' =ᵐ[μ] t' → s \ s' =ᵐ[μ] t \ t'
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.removeNeg_addNeg_cancel : ∀ {assignment : Std.Tactic.BVDecide.LRAT.Internal.Assignment},
  ¬assignment.hasNegAssignment = true → assignment.addNegAssignment.removeNegAssignment = assignment
-- Init.Data.BitVec.Basic
/-- Unsigned less-than for bitvectors.

SMT-LIB name: `bvult`.
 -/
BitVec.ult : {n : ℕ} → BitVec n → BitVec n → Bool
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
/-- **Alias** of `UpperHalfPlane.ext_re_im`.

---

Extensionality lemma in terms of `UpperHalfPlane.re` and `UpperHalfPlane.im`.  -/
UpperHalfPlane.ext' : ∀ {a b : UpperHalfPlane}, a.re = b.re → a.im = b.im → a = b
-- Mathlib.Data.Finsupp.MonomialOrder.DegLex
ofDegLex_inj : ∀ {α : Type u_1} {a b : DegLex α}, ofDegLex a = ofDegLex b ↔ a = b
-- Mathlib.Order.BooleanAlgebra.Set
Set.compl_union : ∀ {α : Type u_1} (s t : Set α), (s ∪ t)ᶜ = sᶜ ∩ tᶜ
-- Mathlib.RingTheory.Norm.Transitivity
/-- `M * aux M k` is upper triangular.  -/
Algebra.Norm.Transitivity.mul_auxMat_blockTriangular : ∀ {S : Type u_2} {m : Type u_5} [inst : CommRing S] (M : Matrix m m S) [inst_1 : DecidableEq m] (k : m)
  [inst_2 : Fintype m], (M * Algebra.Norm.Transitivity.auxMat M k).BlockTriangular fun x => x = k
-- Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits
_private.Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits.0.SimpleGraph.ErdosStone.card_edgeFinset_between_verts_le : ∀ {n : ℕ} {G : SimpleGraph (Fin n)} [inst : DecidableRel G.Adj] {r t t' : ℕ} (K : G.CompleteEquipartiteSubgraph r t'),
  0 < r →
    0 < t' →
      ↑(SimpleGraph.between (↑K.verts) (↑K.verts)ᶜ G).edgeFinset.card ≤
        (↑n - ↑K.verts.card) * (↑K.verts.card - (↑t' - ↑t)) + ↑(SimpleGraph.ErdosStone.filter✝ K t).card * (↑t' - ↑t)
-- Batteries.Data.List.Basic
List.dropSliceTR.go.eq_1 : ∀ {α : Type u_1} (l : List α) (m a : ℕ) (a_1 : Array α), List.dropSliceTR.go l m [] a a_1 = l
-- Mathlib.Data.Complex.Basic
/-- If `s ⊆ s₁ ⊆ ℝ` and `t ⊆ t₁ ⊆ ℝ`, then `s × t ⊆ s₁ × t₁` in `ℂ`.  -/
Complex.reProdIm_subset_iff' : ∀ {s s₁ t t₁ : Set ℝ}, s ×ℂ t ⊆ s₁ ×ℂ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅
-- Mathlib.Algebra.GroupWithZero.Units.Basic
Units.mk0.congr_simp : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] (a a_1 : G₀) (e_a : a = a_1) (ha : a ≠ 0), Units.mk0 a ha = Units.mk0 a_1 ⋯
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas
Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go_eval_eq_eval : ∀ (expr : Std.Tactic.BVDecide.BVLogicalExpr) (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit)
  (assign : Std.Tactic.BVDecide.BVExpr.Assignment) (cache : Std.Tactic.BVDecide.BVExpr.Cache aig),
  Std.Tactic.BVDecide.BVExpr.Cache.Inv assign aig cache →
    ⟦assign.toAIGAssignment, ↑(Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go aig expr cache).result⟧ =
      Std.Tactic.BVDecide.BVLogicalExpr.eval assign expr
-- Mathlib.GroupTheory.SpecificGroups.Quaternion
QuaternionGroup.a : {n : ℕ} → ZMod (2 * n) → QuaternionGroup n
-- Init.Data.Array.Lemmas
List.extract_toArray : ∀ {α : Type u_1} {l : List α} {start stop : ℕ}, l.toArray.extract start stop = (l.extract start stop).toArray
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
/-- As the associator and left and right unitors are defined as eqToIso of category axioms, the
bicategory structure on `CatEnriched C` is strict.  -/
CategoryTheory.CatEnriched.instStrict : ∀ {C : Type u_1} [inst : CategoryTheory.EnrichedCategory CategoryTheory.Cat C],
  CategoryTheory.Bicategory.Strict (CategoryTheory.CatEnriched C)
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.IsCharTwoNF.of_j_ne_zero : ∀ {R : Type u_1} [inst : CommRing R] {W : WeierstrassCurve R} [W.IsCharTwoJNeZeroNF], W.IsCharTwoNF
-- Mathlib.Analysis.Convex.Side
AffineSubspace.wOppSide_smul_vsub_vadd_left : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {p₁ p₂ : P} (x : P), p₁ ∈ s → p₂ ∈ s → ∀ {t : R}, t ≤ 0 → s.WOppSide (t • (x -ᵥ p₁) +ᵥ p₂) x
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.Compacts.secondCountableTopology_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α],
  SecondCountableTopology (TopologicalSpace.Compacts α) ↔ SecondCountableTopology α
-- Mathlib.Data.Fin.Tuple.Finset
Finset.filter_piFinset_eq_map_consEquiv : ∀ {n : ℕ} {α : Fin (n + 1) → Type u_1} (S : (i : Fin (n + 1)) → Finset (α i)) (P : ((i : Fin n) → α i.succ) → Prop)
  [inst : DecidablePred P],
  {r ∈ Fintype.piFinset S | P (Fin.tail r)} =
    Finset.map (Fin.consEquiv α).toEmbedding (S 0 ×ˢ {r ∈ Fintype.piFinset (Fin.tail S) | P r})
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.op_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.IsIso f],
  (CategoryTheory.inv f).op = CategoryTheory.inv f.op
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
/-- The graph of a measurable function is a measurable set.  -/
measurableSet_graph : ∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → ℝ}, Measurable f → MeasurableSet {p | p.2 = f p.1}
-- Mathlib.Order.Disjoint
/-- Two elements of a lattice are disjoint if their inf is the bottom element.
  (This generalizes disjoint sets, viewed as members of the subset lattice.)

Note that we define this without reference to `⊓`, as this allows us to talk about orders where
the infimum is not unique, or where implementing `Inf` would require additional `Decidable`
arguments.  -/
Disjoint : {α : Type u_1} → [inst : PartialOrder α] → [OrderBot α] → α → α → Prop
-- Std.Data.Iterators.Consumers.Set
/-- Traverses the given iterator and stores the emitted values in a `ExtHashSet`.

This variant terminates after finitely many steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using `Iter.toExtHashSet`.
 -/
Std.Iter.Total.toExtHashSet : {α β : Type w} →
  [inst : BEq β] →
    [inst_1 : Hashable β] →
      [EquivBEq β] →
        [LawfulHashable β] →
          [inst_4 : Std.Iterator α Id β] →
            [Std.Iterators.Finite α Id] → [Std.IteratorLoop α Id Id] → Std.Iter.Total β → Std.ExtHashSet β
-- Mathlib.RingTheory.OreLocalization.Basic
OreLocalization.instDistribMulAction : {R : Type u_1} →
  [inst : Monoid R] →
    {S : Submonoid R} →
      [inst_1 : OreLocalization.OreSet S] →
        {X : Type u_2} →
          [inst_2 : AddMonoid X] →
            [inst_3 : DistribMulAction R X] → DistribMulAction (OreLocalization S R) (OreLocalization S X)
-- Mathlib.RingTheory.QuotSMulTop
QuotSMulTop.mem_annihilator : ∀ {R : Type u_2} [inst : CommRing R] (M : Type u_1) [inst_1 : AddCommGroup M] [inst_2 : Module R M] (x : R),
  x ∈ Module.annihilator R (QuotSMulTop x M)
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.instDecidableMapAdj : {V : Type u_1} →
  {W : Type u_2} →
    (G : SimpleGraph V) →
      [DecidableEq W] →
        {f : V → W} → {a b : W} → [Decidable (Relation.Map G.Adj f f a b)] → Decidable ((SimpleGraph.map f G).Adj a b)
-- Init.Data.List.Lemmas
List.ne_nil_iff_exists_cons : ∀ {α : Type u_1} {l : List α}, l ≠ [] ↔ ∃ b l', l = b :: l'
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKeyD_erase_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k fallback : α}, (m.erase k).getKeyD k fallback = fallback
-- Std.Http.Data.URI.Basic
Std.Http.URI.instReprPort.repr : Std.Http.URI.Port → ℕ → Std.Format
-- Mathlib.CategoryTheory.Limits.Types.Filtered
CategoryTheory.Limits.Types.FilteredColimit.colimit_eq_iff_aux : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u))
  [CategoryTheory.IsFilteredOrEmpty J] [inst_2 : CategoryTheory.Limits.HasColimit F] {i j : J} {xi : F.obj i}
  {xj : F.obj j},
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Limits.Types.colimitCocone F).ι.app i)) xi =
      (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Limits.Types.colimitCocone F).ι.app j)) xj ↔
    CategoryTheory.Limits.Types.FilteredColimit.Rel F ⟨i, xi⟩ ⟨j, xj⟩
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.Option.isSome.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : (val : α) → motive (some val)) (h_2 : Unit → motive none),
  (match none with
    | some val => h_1 val
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Over.homMk.congr_simp : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T} {X : T}
  [inst_1 : Q.IsMultiplicative] {A B : P.Over Q X} (f f_1 : A.left ⟶ B.left) (e_f : f = f_1)
  (w : CategoryTheory.CategoryStruct.comp f B.hom = A.hom) (hf : Q f),
  CategoryTheory.MorphismProperty.Over.homMk f w hf = CategoryTheory.MorphismProperty.Over.homMk f_1 ⋯ ⋯
-- Mathlib.CategoryTheory.Functor.Category
CategoryTheory.NatTrans.naturality_app_app_assoc : ∀ {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] {E' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E']
  {F G : CategoryTheory.Functor C (CategoryTheory.Functor D (CategoryTheory.Functor E E'))} (α : F ⟶ G) {X₁ Y₁ : C}
  (f : X₁ ⟶ Y₁) (X₂ : D) (X₃ : E) {Z : E'} (h : ((G.obj Y₁).obj X₂).obj X₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (((F.map f).app X₂).app X₃)
      (CategoryTheory.CategoryStruct.comp (((α.app Y₁).app X₂).app X₃) h) =
    CategoryTheory.CategoryStruct.comp (((α.app X₁).app X₂).app X₃)
      (CategoryTheory.CategoryStruct.comp (((G.map f).app X₂).app X₃) h)
-- Mathlib.Algebra.Module.Submodule.Ker
/-- The increasing sequence of submodules consisting of the kernels of the iterates of a linear map.
 -/
LinearMap.iterateKer : {R : Type u_1} →
  {M : Type u_5} →
    [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → (M →ₗ[R] M) → ℕ →o Submodule R M
-- Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
/-- If an element `x` is a root of a nonzero polynomial `p`, then the degree of `p` is at least the
degree of the minimal polynomial of `x`. See also `minpoly.degree_le_of_ne_zero` which relaxes the
assumptions on `S` in exchange for stronger assumptions on `R`.  -/
minpoly.IsIntegrallyClosed.degree_le_of_ne_zero : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [IsDomain R] [inst_3 : Algebra R S]
  [IsIntegrallyClosed R] [IsDomain S] [Module.IsTorsionFree R S] {s : S} {p : Polynomial R},
  p ≠ 0 → (Polynomial.aeval s) p = 0 → (minpoly R s).degree ≤ p.degree
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestMatchAt.le : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice}
  {startPos endPos : s.Pos}, String.Slice.Pattern.Model.IsLongestMatchAt pat startPos endPos → startPos ≤ endPos
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Context.setAutoUnfold : Lean.Meta.Simp.Context → Lean.Meta.Simp.Context
-- Lean.Elab.Do.Basic
Lean.Elab.Do.mkMonadicResultTypeMismatchError : Lean.Expr → Lean.Expr → Lean.MessageData
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.smul_mem_iff : ∀ {𝕜 : Type u_1} {M : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommMonoid M] [inst_4 : MulAction 𝕜 M] (C : ConvexCone 𝕜 M) {c : 𝕜}, 0 < c → ∀ {x : M}, c • x ∈ C ↔ x ∈ C
-- Mathlib.NumberTheory.DirichletCharacter.Basic
/-- Let `χ` and `ψ` be Dirichlet characters of level `n` and `m` respectively. Assume that they agree
at level `n * m`. Then `χ` factors through `gcd(n, m)`.
 -/
DirichletCharacter.factorsThrough_gcd : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) {m : ℕ} [NeZero n]
  (ψ : DirichletCharacter R m),
  (DirichletCharacter.changeLevel ⋯) χ = (DirichletCharacter.changeLevel ⋯) ψ → χ.FactorsThrough (n.gcd m)
-- Mathlib.Algebra.Group.Action.Prod
Prod.faithfulSMulRight : ∀ {M : Type u_1} {α : Type u_5} {β : Type u_6} [inst : SMul M α] [inst_1 : SMul M β] [Nonempty α] [FaithfulSMul M β],
  FaithfulSMul M (α × β)
-- Mathlib.MeasureTheory.Integral.DominatedConvergence
MeasureTheory.IntegrableOn.continuousOn_Iic_primitive_Iic : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {μ : MeasureTheory.Measure ℝ} {f : ℝ → E}
  [MeasureTheory.NullSingletonClass μ] {a₀ : ℝ},
  MeasureTheory.IntegrableOn f (Set.Iic a₀) μ → ContinuousOn (fun b => ∫ (x : ℝ) in Set.Iic b, f x ∂μ) (Set.Iic a₀)
-- Mathlib.GroupTheory.Commutator.Basic
/-- If `N` is a normal subgroup of `G` and `H` a commutative subgroup such that `H ⊔ N = ⊤`,
then `N` contains `commutator G`.  -/
Subgroup.Normal.commutator_le_of_self_sup_commutative_eq_top : ∀ {G : Type u_1} [inst : Group G] {N : Subgroup G} [N.Normal] {H : Subgroup G},
  N ⊔ H = ⊤ → IsMulCommutative ↥H → commutator G ≤ N
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PushoutCocone.flip_inl : ∀ {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.flip.inl = t.inr
-- Mathlib.Geometry.Manifold.Algebra.Monoid
instInhabitedContMDiffAddMonoidMorphism : {𝕜 : 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'] →
                                              Inhabited (ContMDiffAddMonoidMorphism I I' n G G')
-- Mathlib.RingTheory.Localization.Pi
IsLocalization.iff_map_piEvalRingHom : ∀ {ι : Type u_1} (R : ι → Type u_2) [inst : (i : ι) → CommSemiring (R i)] (S' : Type u_4) [inst_1 : CommSemiring S']
  [inst_2 : Algebra ((i : ι) → R i) S'] (M : Submonoid ((i : ι) → R i)) [Finite ι],
  IsLocalization M S' ↔ IsLocalization (Submonoid.pi Set.univ fun i => Submonoid.map (Pi.evalRingHom R i) M) S'
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.Hom.minDegree_mono : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [inst : Fintype V] [inst_1 : Fintype W]
  [inst_2 : DecidableRel G.Adj] [inst_3 : DecidableRel H.Adj] {f : G →g H},
  Function.Bijective ⇑f → G.minDegree ≤ H.minDegree
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.comp_smul : ∀ {R : Type r} [inst : CommRing R] {S : Type s} [inst_1 : CommRing S] (f : R →+* S) (P : Fin 3 → R) (u : R),
  ⇑f ∘ (u • P) = f u • ⇑f ∘ P