mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Cover.Over
AlgebraicGeometry.Scheme.Cover.pullbackCoverOver_f : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme)
  [inst : P.IsStableUnderBaseChange] [inst_1 : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P]
  {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X)
  (f : W ⟶ X) [inst_2 : W.Over S] [inst_3 : X.Over S] [inst_4 : AlgebraicGeometry.Scheme.Cover.Over S 𝒰]
  [inst_5 : AlgebraicGeometry.Scheme.Hom.IsOver f S] (x : 𝒰.I₀),
  (AlgebraicGeometry.Scheme.Cover.pullbackCoverOver S 𝒰 f).f x =
    CategoryTheory.Over.Hom.left
      (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Hom.asOver f S)
        (AlgebraicGeometry.Scheme.Hom.asOver (𝒰.f x) S))
-- Mathlib.Topology.Constructions.SumProd
Homeomorph.sumSumSumComm_symm : ∀ (X : Type u) (Y : Type v) (W : Type u_1) (Z : Type u_2) [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace W] [inst_3 : TopologicalSpace Z],
  (Homeomorph.sumSumSumComm X Y W Z).symm = Homeomorph.sumSumSumComm X W Y Z
-- Mathlib.SetTheory.Ordinal.Notation
ONote.eq_of_cmp_eq : ∀ {o₁ o₂ : ONote}, o₁.cmp o₂ = Ordering.eq → o₁ = o₂
-- Init.MetaTypes
Lean.Meta.instBEqTransparencyMode.beq : Lean.Meta.TransparencyMode → Lean.Meta.TransparencyMode → Bool
-- Std.Data.Iterators.Lemmas.Producers.Slice
Std.Slice.iter_eq_toIteratorIter : ∀ {α β : Type v} {γ : Type u} {s : Std.Slice γ} [inst : Std.ToIterator (Std.Slice γ) Id α β],
  s.iter = Std.ToIterator.iter s
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddSubmonoid.LocalizationMap.ofAddEquivOfLocalizations.eq_1 : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) (k : N ≃+ P),
  f.ofAddEquivOfLocalizations k = (k.toAddMonoidHom.comp f.toAddMonoidHom).toLocalizationMap ⋯ ⋯ ⋯
-- Mathlib.RingTheory.LocalProperties.Basic
/-- A property `P` of ring homs satisfies `RingHom.OfLocalizationFiniteSpan`
if `P` holds for `R →+* S` whenever there exists a finite set `{ r }` that spans `R` such that
`P` holds for `Rᵣ →+* Sᵣ`.

Note that this is equivalent to `RingHom.OfLocalizationSpan` via
`RingHom.ofLocalizationSpan_iff_finite`, but this is easier to prove.  -/
RingHom.OfLocalizationFiniteSpan : ({R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) → Prop
-- Mathlib.RepresentationTheory.FDRep
/-- The category of finitely generated `R`-linear representations of a monoid `G`.

Note that `R` can be any ring,
but the main case of interest is when `R = k` is a field and `G` is a group.  -/
FDRep : (R : Type u) → (G : Type v) → [Ring R] → [Monoid G] → Type (max (max (u + 1) v) u)
-- Mathlib.Control.Monad.Cont
ContT.instMonadCont : {r : Type u} → {m : Type u → Type v} → MonadCont (ContT r m)
-- Mathlib.Data.Multiset.ZeroCons
Multiset.cons_ne_zero : ∀ {α : Type u_1} {a : α} {m : Multiset α}, a ::ₘ m ≠ 0
-- Mathlib.Topology.Algebra.Group.GroupTopology
AddGroupTopology.ext' : ∀ {α : Type u} [inst : AddGroup α] {f g : AddGroupTopology α}, TopologicalSpace.IsOpen = TopologicalSpace.IsOpen → f = g
-- Aesop.Tree.AddRapp
Aesop.copyGoals : Aesop.UnorderedArraySet Lean.MVarId →
  Aesop.GoalRef → Lean.Meta.SavedState → Aesop.Percent → ℕ → Aesop.TreeM (Array Aesop.Goal)
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Measurable.subset : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace β] [Countable α] {s t : β → Set α},
  Measurable s → Measurable t → Measurable fun a => s a ⊆ t a
-- Mathlib.Analysis.Normed.Module.ContinuousInverse
ContinuousLinearMap.HasLeftInverse.isCompl_complement : ∀ {R : Type u_7} {E : Type u_8} {F : Type u_10} [inst : Ring R] [inst_1 : TopologicalSpace E] [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] [inst_4 : TopologicalSpace F] [inst_5 : AddCommGroup F] [inst_6 : Module R F] {f : E →L[R] F}
  (h : f.HasLeftInverse), IsCompl (↑f).range h.complement
-- Mathlib.GroupTheory.NoncommPiCoprod
Subgroup.commute_subtype_of_commute : ∀ {G : Type u_1} [inst : Group G] {ι : Type u_2} {H : ι → Subgroup G},
  (Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y) →
    ∀ (i j : ι), i ≠ j → ∀ (x : ↥(H i)) (y : ↥(H j)), Commute ((H i).subtype x) ((H j).subtype y)
-- Mathlib.LinearAlgebra.FreeModule.Basic
Module.Free.of_subsingleton' : ∀ (R : Type u) (N : Type z) [inst : Semiring R] [inst_1 : AddCommMonoid N] [inst_2 : Module R N] [Subsingleton R],
  Module.Free R N
-- Batteries.Data.String.Legacy
/-- Returns the position of the first occurrence of a character, `c`, in a string `s`. If `s` does not
contain `c`, returns `s.rawEndPos`.

This is an old implementation, preserved here for users of the lemmas in
`Batteries.Data.String.Lemmas`.

Examples:
* `"abcba".posOf 'a' = ⟨0⟩`
* `"abcba".posOf 'z' = ⟨5⟩`
* `"L∃∀N".posOf '∀' = ⟨4⟩`
 -/
String.Legacy.posOf : String → Char → String.Pos.Raw
-- Init.Data.Range.Polymorphic.NatLemmas
Std.PRange.Nat.toList_Rco_succ_succ : ∀ {m n : ℕ}, ((m + 1)...n + 1).toList = List.map (fun x => x + 1) (m...n).toList
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.Const.insertMany : {α : Type u} →
  {β : Type v} →
    {ρ : Type w} →
      [ForIn Id ρ (α × β)] →
        [inst : BEq α] →
          [inst_1 : Hashable α] →
            (m : Std.DHashMap.Internal.Raw₀ α fun x => β) →
              ρ →
                { m' //
                  ∀ (P : (Std.DHashMap.Internal.Raw₀ α fun x => β) → Prop),
                    (∀ {m'' : Std.DHashMap.Internal.Raw₀ α fun x => β} {a : α} {b : β}, P m'' → P (m''.insert a b)) →
                      P m → P m' }
-- Std.Http.Data.URI.Basic
/-- The path segments making up the hierarchical structure (each segment is percent-encoded).
 -/
Std.Http.URI.Path.segments : Std.Http.URI.Path → Array Std.Http.URI.EncodedSegment
-- Mathlib.Algebra.Order.Field.Power
zpow_eq_zpow_iff_of_ne_zero₀ : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a b : α} {n : ℤ},
  n ≠ 0 → (a ^ n = b ^ n ↔ a = b ∨ a = -b ∧ Even n)
-- Mathlib.RingTheory.Spectrum.Prime.RingHom
PrimeSpectrum.residueField_comap : ∀ {R : Type u_1} [inst : CommRing R] (I : PrimeSpectrum R),
  Set.range (PrimeSpectrum.comap (algebraMap R I.asIdeal.ResidueField)) = {I}
-- Mathlib.Data.Real.ConjExponents
NNReal.HolderTriple.inv_pos : ∀ {p q r : NNReal}, p.HolderTriple q r → 0 < p⁻¹
-- Mathlib.Data.Vector.Snoc
List.Vector.snoc_nil : ∀ {α : Type u_1} {x : α}, List.Vector.nil.snoc x = x ::ᵥ List.Vector.nil
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.Iteration.mapObj_trans_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C}
  [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J]
  [inst_4 : CategoryTheory.Limits.HasIterationOfShape J C] [inst_5 : WellFoundedLT J] {j₁ j₂ j₃ : J}
  (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) (iter₃ : Φ.Iteration j₃) {k₁ k₂ k₃ : J} (h₁₂ : k₁ ≤ k₂)
  (h₂₃ : k₂ ≤ k₃) (h₁ : k₁ ≤ j₁) (h₂ : k₂ ≤ j₂) (h₃ : k₃ ≤ j₃) (h₁₂' : j₁ ≤ j₂) (h₂₃' : j₂ ≤ j₃) {Z : C}
  (h : iter₃.F.obj ⟨k₃, h₃⟩ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (iter₁.mapObj iter₂ h₁₂ h₁ h₂ h₁₂')
      (CategoryTheory.CategoryStruct.comp (iter₂.mapObj iter₃ h₂₃ h₂ h₃ h₂₃') h) =
    CategoryTheory.CategoryStruct.comp (iter₁.mapObj iter₃ ⋯ h₁ h₃ ⋯) h
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.indep_congr : ∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {m₁ m₂ _mΩ : MeasurableSpace Ω}
  {κ η : ProbabilityTheory.Kernel α Ω},
  ⇑κ =ᵐ[μ] ⇑η → (ProbabilityTheory.Kernel.Indep m₁ m₂ κ μ ↔ ProbabilityTheory.Kernel.Indep m₁ m₂ η μ)
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_counitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z},
  CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan.counitIso =
    CategoryTheory.NatIso.ofComponents
      (fun X_1 =>
        CategoryTheory.Limits.BinaryCofan.ext
          (CategoryTheory.Under.isoMk
            (CategoryTheory.Iso.refl
              (({
                            obj := fun c =>
                              CategoryTheory.Limits.PushoutCocone.mk (CategoryTheory.Under.Hom.right c.inl)
                                (CategoryTheory.Under.Hom.right c.inr) ⋯,
                            map := fun {c₁ c₂} a => { hom := CategoryTheory.Under.Hom.right a.hom, w := ⋯ },
                            map_id := ⋯, map_comp := ⋯ }.comp
                        {
                          obj := fun c =>
                            CategoryTheory.Limits.BinaryCofan.mk (CategoryTheory.Under.homMk c.inl ⋯)
                              (CategoryTheory.Under.homMk c.inr ⋯),
                          map := fun {c₁ c₂} a => { hom := CategoryTheory.Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯,
                          map_comp := ⋯ }).obj
                    X_1).pt.right)
            ⋯)
          ⋯ ⋯)
      ⋯
-- Init.Grind.Norm
Lean.Grind.not_forall : ∀ {α : Sort u_1} (p : α → Prop), (¬∀ (x : α), p x) = ∃ x, ¬p x
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.instToFormatStackEntry : Std.ToFormat Lean.Meta.RefinedDiscrTree.StackEntry
-- Mathlib.Algebra.MvPolynomial.Division
MvPolynomial.mul_monomial_modMonomial : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (s : σ →₀ ℕ) (x : MvPolynomial σ R),
  (x * (MvPolynomial.monomial s) 1).modMonomial s = 0
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
/-- If the pullback comparison map for `G` at `(f,g)` is an isomorphism, then `G` preserves the
pullback of `(f,g)`.  -/
CategoryTheory.Limits.PreservesPullback.of_iso_comparison : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [inst_2 : CategoryTheory.Limits.HasPullback f g]
  [inst_3 : CategoryTheory.Limits.HasPullback (G.map f) (G.map g)]
  [i : CategoryTheory.IsIso (CategoryTheory.Limits.pullbackComparison G f g)],
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) G
-- Init.Data.UInt.Lemmas
UInt64.toFin_mod : ∀ (a b : UInt64), (a % b).toFin = a.toFin % b.toFin
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Filtered
CategoryTheory.Limits.instHasFilteredColimitsOfSizeFunctor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  [CategoryTheory.Limits.HasFilteredColimitsOfSize.{w', w, v₁, u₁} C],
  CategoryTheory.Limits.HasFilteredColimitsOfSize.{w', w, max u₂ v₁, max (max (max u₁ u₂) v₁) v₂}
    (CategoryTheory.Functor K C)
-- Mathlib.Order.LiminfLimsup
Filter.liminf_le_limsup_of_frequently_le : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLinearOrder β] {f : Filter α} {u v : α → β},
  (∃ᶠ (x : α) in f, u x ≤ v x) →
    autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) Filter.liminf_le_limsup_of_frequently_le._auto_1 →
      autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v) Filter.liminf_le_limsup_of_frequently_le._auto_3 →
        Filter.liminf u f ≤ Filter.limsup v f
-- Init.Data.UInt.Lemmas
UInt8.size_dvd_usizeSize : UInt8.size ∣ USize.size
-- Lean.Meta.Tactic.Symm
/-- Apply a symmetry lemma (i.e. marked with `@[symm]`) to a metavariable.

The type of `g` should be of the form `a ~ b`, and is used to index the symm lemmas.
 -/
Lean.MVarId.applySymm : Lean.MVarId → Lean.MetaM Lean.MVarId
-- Mathlib.GroupTheory.GroupAction.Hom
/-- Composition of two equivariant monoid homomorphisms.  -/
MulDistribMulActionHom.comp : {M : Type u_1} →
  [inst : Monoid M] →
    {N : Type u_2} →
      [inst_1 : Monoid N] →
        {P : Type u_3} →
          [inst_2 : Monoid P] →
            {φ : M →* N} →
              {ψ : N →* P} →
                {χ : M →* P} →
                  {A : Type u_4} →
                    [inst_3 : Monoid A] →
                      [inst_4 : MulDistribMulAction M A] →
                        {B : Type u_5} →
                          [inst_5 : Monoid B] →
                            [inst_6 : MulDistribMulAction N B] →
                              {C : Type u_7} →
                                [inst_7 : Monoid C] →
                                  [inst_8 : MulDistribMulAction P C] →
                                    [κ : φ.CompTriple ψ χ] → (B →ₑ*[ψ] C) → (A →ₑ*[φ] B) → A →ₑ*[χ] C
-- Mathlib.Algebra.Lie.Weights.Basic
/-- This lemma exists only to simplify the proof of
`LieModule.isCompl_genWeightSpace_zero_posFittingComp`.  -/
_private.Mathlib.Algebra.Lie.Weights.Basic.0.LieModule.isCompl_genWeightSpace_zero_posFittingComp_aux : ∀ (R : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [IsNoetherian R M] [IsArtinian R M],
  (∀ N < ⊤, IsCompl (LieModule.genWeightSpace (↥N) 0) (LieModule.posFittingComp R L ↥N)) →
    IsCompl (LieModule.genWeightSpace M 0) (LieModule.posFittingComp R L M)
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.frameHom_toFun : ∀ {α : Type u_2} [inst : TopologicalSpace α] (x : TopologicalSpace.Opens α), TopologicalSpace.Opens.frameHom x = ↑x
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.comp : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.IsOpenImmersion f]
  [AlgebraicGeometry.IsOpenImmersion g], AlgebraicGeometry.IsOpenImmersion (CategoryTheory.CategoryStruct.comp f g)
-- Lean.Meta.SizeOf
Lean.Meta.SizeOfSpecNested.Context.localInsts : Lean.Meta.SizeOfSpecNested.Context → Array Lean.Expr
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.postcompose_obj_pt : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} (α : F ⟶ G) (c : CategoryTheory.Limits.Cone F),
  ((CategoryTheory.Limits.Cone.postcompose α).obj c).pt = c.pt
-- Lean.Parser.Syntax
Lean.Parser.Syntax.numPrec.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Star.Pointwise
Set.star_inv : ∀ {α : Type u_1} [inst : Group α] [inst_1 : StarMul α] (s : Set α), star s⁻¹ = (star s)⁻¹
-- Mathlib.Analysis.Normed.Affine.AddTorsorBases
IsOpen.exists_subset_affineIndependent_span_eq_top : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {u : Set P},
  IsOpen u → u.Nonempty → ∃ s ⊆ u, AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ s = ⊤
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- Order equivalence between blocks in `X` containing a point `a`
and subgroups of `G` containing the stabilizer of `a` (Wielandt, th. 7.5)  -/
AddAction.block_stabilizerOrderIso : (G : Type u_1) →
  [inst : AddGroup G] →
    {X : Type u_2} →
      [inst_1 : AddAction G X] →
        [htGX : AddAction.IsPretransitive G X] →
          (a : X) → { B // a ∈ B ∧ AddAction.IsBlock G B } ≃o ↑(Set.Ici (AddAction.stabilizer G a))
-- Lean.Elab.DocString
/-- Context used as a reader in `DocM`.  -/
Lean.Doc.Context : Type
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.preimage_floor_of_ne_zero : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] [IsStrictOrderedRing R]
  {n : ℕ}, n ≠ 0 → Nat.floor ⁻¹' {n} = Set.Ico (↑n) (↑n + 1)
-- Mathlib.Algebra.BigOperators.Pi
Finset.prod_apply : ∀ {ι : Type u_1} {α : Type u_7} {M : α → Type u_8} [inst : (a : α) → CommMonoid (M a)] (a : α) (s : Finset ι)
  (g : ι → (a : α) → M a), (∏ c ∈ s, g c) a = ∏ c ∈ s, g c a
-- Init.Meta.Defs
Lean.Meta.instReprEtaStructMode.repr : Lean.Meta.EtaStructMode → ℕ → Std.Format
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.inter_add_subset : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α] {s₁ s₂ t : Finset α}, s₁ ∩ s₂ + t ⊆ (s₁ + t) ∩ (s₂ + t)
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
ExteriorAlgebra.invertibleAlgebraMapEquiv_apply_invOf : ∀ {R : Type u1} [inst : CommRing R] (M : Type u2) [inst_1 : AddCommGroup M] [inst_2 : Module R M] (r : R)
  (x : Invertible ((algebraMap R (ExteriorAlgebra R M)) r)),
  ⅟r = ⅟(ExteriorAlgebra.algebraMapInv ((algebraMap R (ExteriorAlgebra R M)) r))
-- Mathlib.Topology.MetricSpace.Holder
HolderWith.dist_le_of_le : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoMetricSpace X] [inst_1 : PseudoMetricSpace Y] {C r : NNReal} {f : X → Y},
  HolderWith C r f → ∀ {x y : X} {d : ℝ}, dist x y ≤ d → dist (f x) (f y) ≤ ↑C * d ^ ↑r
-- Mathlib.Order.Monotone.Basic
monotoneOn_nat_Ici_of_le_succ : ∀ {α : Type u} [inst : Preorder α] {f : ℕ → α} {k : ℕ}, (∀ n ≥ k, f n ≤ f (n + 1)) → MonotoneOn f {x | k ≤ x}
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.instZero.eq_1 : ∀ {α : Type u}, WithZero.instZero = { zero := none }
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.mk_coe : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (e' : A₂ → A₁) (h₁ : Function.LeftInverse e' ⇑e)
  (h₂ : Function.RightInverse e' ⇑e)
  (h₃ :
    ∀ (x y : A₁),
      { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun (x * y) =
        { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun x *
          { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun y)
  (h₄ :
    ∀ (x y : A₁),
      { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun (x + y) =
        { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun x +
          { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun y)
  (h₅ :
    ∀ (r : R),
      { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun ((algebraMap R A₁) r) = (algebraMap R A₂) r),
  { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄, commutes' := h₅ } = e
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instRing : {n : Type u_2} → {A : Type u_5} → [Fintype n] → [DecidableEq n] → [Ring A] → Ring (CStarMatrix n n A)
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.app'.injEq : ∀ (a a_1 a_2 a_3 : Mathlib.Tactic.ITauto.Proof), (a.app' a_1 = a_2.app' a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.instEquivLike : {M : Type u_4} → {N : Type u_5} → [inst : Mul M] → [inst_1 : Mul N] → EquivLike (M ≃* N) M N
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.coeffs_one : ∀ {R : Type u} [inst : Semiring R], Polynomial.coeffs 1 ⊆ {1}
-- Mathlib.Tactic.NormNum.Result
/-- Untyped version of `Result.isNat`.  -/
Mathlib.Meta.NormNum.Result'.isNat : Lean.Expr → Lean.Expr → Lean.Expr → Mathlib.Meta.NormNum.Result'
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.App.State : Type
-- Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
CategoryTheory.strongMono_of_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q : C} [CategoryTheory.StrongMonoCategory C] (f : Q ⟶ P)
  [CategoryTheory.Mono f], CategoryTheory.StrongMono f
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey?_erase!_eq_of_not_compare_eq_minKey? : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α},
      (∀ {km : α}, t.minKey? = some km → ¬compare k km = Ordering.eq) →
        (Std.DTreeMap.Internal.Impl.erase! k t).minKey? = t.minKey?
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
ProfiniteAddGrp.ProfiniteCompletion.quotientMap.eq_1 : ∀ {G : AddGrpCat} {P : ProfiniteAddGrp.{u}} (f : G ⟶ AddGrpCat.of ↑P.toProfinite.toTop)
  (H : OpenNormalAddSubgroup ↑P.toProfinite.toTop),
  ProfiniteAddGrp.ProfiniteCompletion.quotientMap f H =
    FiniteAddGrp.ofHom
      (QuotientAddGroup.map (ProfiniteAddGrp.ProfiniteCompletion.preimage f H).toAddSubgroup (↑H.toOpenAddSubgroup)
        (AddGrpCat.Hom.hom f) ⋯)
-- Lean.Meta.Instances
Lean.Meta.InstanceEntry.mk.inj : ∀ {keys : Array Lean.Meta.InstanceKey} {val : Lean.Expr} {priority : ℕ} {globalName? : Option Lean.Name}
  {synthOrder : Array ℕ} {attrKind : Lean.AttributeKind} {keys_1 : Array Lean.Meta.InstanceKey} {val_1 : Lean.Expr}
  {priority_1 : ℕ} {globalName?_1 : Option Lean.Name} {synthOrder_1 : Array ℕ} {attrKind_1 : Lean.AttributeKind},
  { keys := keys, val := val, priority := priority, globalName? := globalName?, synthOrder := synthOrder,
        attrKind := attrKind } =
      { keys := keys_1, val := val_1, priority := priority_1, globalName? := globalName?_1, synthOrder := synthOrder_1,
        attrKind := attrKind_1 } →
    keys = keys_1 ∧
      val = val_1 ∧
        priority = priority_1 ∧ globalName? = globalName?_1 ∧ synthOrder = synthOrder_1 ∧ attrKind = attrKind_1
-- Mathlib.Order.Fin.Tuple
Fin.insertNthOrderIso.eq_1 : ∀ {n : ℕ} (α : Fin (n + 1) → Type u_2) [inst : (i : Fin (n + 1)) → LE (α i)] (p : Fin (n + 1)),
  Fin.insertNthOrderIso α p = { toEquiv := Fin.insertNthEquiv α p, map_rel_iff' := ⋯ }
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.ext : ∀ {𝕜 : 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} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Monoid G] [inst_7 : ContMDiffMul I (↑⊤) G]
  {X Y : LeftInvariantDerivation I G}, (∀ (f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤), X f = Y f) → X = Y
-- Mathlib.GroupTheory.IsSubnormal
_private.Mathlib.GroupTheory.IsSubnormal.0.Subgroup.IsSubnormal.isSubnormal_iff.match_1_1.congr_eq_1 : ∀ (motive : ℕ → Sort u_1) (x : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  x = 0 →
    (match x with
      | 0 => h_1 ()
      | n.succ => h_2 n) ≍
      h_1 ()
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
SSet.ιNormalizedChainComplex_fromNormalizedChainComplex_f_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) {R : C} {n : ℕ} (x : X.obj (Opposite.op { len := n })) {Z : C}
  (h : (X.chainComplex R).X n ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.ιNormalizedChainComplex x)
      (CategoryTheory.CategoryStruct.comp ((X.fromNormalizedChainComplex R).f n) h) =
    CategoryTheory.CategoryStruct.comp (X.ιChainComplex x)
      (CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f n) h)
-- Mathlib.Topology.Path
Path.cast.congr_simp : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} (γ γ_1 : Path x y),
  γ = γ_1 → ∀ {x' y' : X} (hx : x' = x) (hy : y' = y), γ.cast hx hy = γ_1.cast hx hy
-- Mathlib.NumberTheory.Dioph
Dioph.reindex_diophFn : ∀ {α β : Type u} {f : (α → ℕ) → ℕ} (g : α → β), Dioph.DiophFn f → Dioph.DiophFn fun v => f (v ∘ g)
-- Init.SizeOf
PLift.up.sizeOf_spec : ∀ {α : Sort u} [inst : SizeOf α] (down : α), sizeOf { down := down } = 1 + sizeOf down
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Algebra.IsQuadraticExtension.mk : ∀ {R : Type u_2} {S : Type u_3} [inst : CommSemiring R] [inst_1 : StrongRankCondition R] [inst_2 : Semiring S]
  [inst_3 : Algebra R S] [toFree : Module.Free R S], Module.finrank R S = 2 → Algebra.IsQuadraticExtension R S
-- Mathlib.Geometry.Manifold.StructureGroupoid
/-- Membership in a structure groupoid respects the equivalence of open partial homeomorphisms.  -/
StructureGroupoid.mem_of_eqOnSource' : ∀ {H : Type u_2} [inst : TopologicalSpace H] (self : StructureGroupoid H) (e e' : OpenPartialHomeomorph H H),
  e ∈ self.members → e' ≈ e → e' ∈ self.members
-- Std.Data.HashMap.Lemmas
Std.HashMap.getThenInsertIfNew?_snd : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {k : α} {v : β},
  (m.getThenInsertIfNew? k v).2 = m.insertIfNew k v
-- Init.Data.UInt.Lemmas
UInt16.ofFin_le_iff_le : ∀ {a b : Fin UInt16.size}, UInt16.ofFin a ≤ UInt16.ofFin b ↔ a ≤ b