mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.ITauto
/-- `itauto` solves the main goal when it is a tautology of intuitionistic propositional logic.
Unlike `grind` and `tauto!` this tactic never uses the law of excluded middle (without the `!`
option), and the proof search is tailored for this use case. `itauto` is complete for intuitionistic
propositional logic: it will solve any goal that is provable in this logic.

* `itauto [a, b]` will additionally attempt case analysis on `a` and `b` assuming that it can derive
  `Decidable a` and `Decidable b`.
* `itauto *` will case on all decidable propositions that it can find among the atomic propositions.
* `itauto!` will work as a classical SAT solver, but the algorithm is not very good in this
  situation.
* `itauto! *` will case on all propositional atoms. *Warning:* This can blow up the proof search, so
  it should be used sparingly.

Example:
```lean
example (p : Prop) : ¬ (p ↔ ¬ p) := by itauto
```
 -/
Mathlib.Tactic.ITauto.itauto : Lean.ParserDescr
-- Mathlib.AlgebraicGeometry.Morphisms.Integral
AlgebraicGeometry.IsIntegralHom.instFstScheme : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [AlgebraicGeometry.IsIntegralHom g],
  AlgebraicGeometry.IsIntegralHom (CategoryTheory.Limits.pullback.fst f g)
-- Mathlib.Algebra.Order.Floor.Defs
/-- `⌊a⌋₊` is the greatest natural `n` such that `n ≤ a`. If `a` is negative, then `⌊a⌋₊ = 0`.  -/
Nat.floor : {α : Type u_2} → [inst : Semiring α] → [inst_1 : PartialOrder α] → [FloorSemiring α] → α → ℕ
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
/-- `SpecΓIdentity` is iso so these are mutually two-sided inverses.  -/
AlgebraicGeometry.ΓSpec.right_triangle : ∀ (R : CommRingCat),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.identityToΓSpec.app (AlgebraicGeometry.Spec.toLocallyRingedSpace.obj (Opposite.op R)))
      (AlgebraicGeometry.Spec.toLocallyRingedSpace.map
        (AlgebraicGeometry.LocallyRingedSpace.SpecΓIdentity.inv.app R).op) =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.Functor.id AlgebraicGeometry.LocallyRingedSpace).obj
        (AlgebraicGeometry.Spec.toLocallyRingedSpace.obj (Opposite.op R)))
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
lt_of_mul_lt_of_one_le_right : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulRightMono α] {a b c : α}, a * b < c → 1 ≤ a → b < c
-- Mathlib.CategoryTheory.Limits.ExactFunctor
CategoryTheory.RightExactFunctor.whiskeringRight_obj_obj_obj : ∀ (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 : D ⥤ᵣ E) (X : C ⥤ᵣ D),
  (((CategoryTheory.RightExactFunctor.whiskeringRight C D E).obj F).obj X).obj = X.obj.comp F.obj
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
/-- Constructor for natural transformations between cospans.  -/
CategoryTheory.Limits.cospanHomMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F G : CategoryTheory.Functor CategoryTheory.Limits.WalkingCospan C} →
      (z : F.obj CategoryTheory.Limits.WalkingCospan.one ⟶ G.obj CategoryTheory.Limits.WalkingCospan.one) →
        (l : F.obj CategoryTheory.Limits.WalkingCospan.left ⟶ G.obj CategoryTheory.Limits.WalkingCospan.left) →
          (r : F.obj CategoryTheory.Limits.WalkingCospan.right ⟶ G.obj CategoryTheory.Limits.WalkingCospan.right) →
            autoParam
                (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingCospan.Hom.inl) z =
                  CategoryTheory.CategoryStruct.comp l (G.map CategoryTheory.Limits.WalkingCospan.Hom.inl))
                CategoryTheory.Limits.cospanHomMk._auto_1 →
              autoParam
                  (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingCospan.Hom.inr) z =
                    CategoryTheory.CategoryStruct.comp r (G.map CategoryTheory.Limits.WalkingCospan.Hom.inr))
                  CategoryTheory.Limits.cospanHomMk._auto_3 →
                (F ⟶ G)
-- Mathlib.Analysis.Convex.NNReal
NNReal.convex_iff : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : Module ℝ M] {s : Set M}, Convex NNReal s ↔ Convex ℝ s
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.equiv_snd_eq_iff_rightCosetEquivalence : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {T : Set G} (hHT : Subgroup.IsComplement (↑H) T) {g₁ g₂ : G},
  (hHT.equiv g₁).2 = (hHT.equiv g₂).2 ↔ RightCosetEquivalence (↑H) g₁ g₂
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.lowerBound?_mem_toList : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x y : α} {t : RBTree.RBSet α cmp}, t.lowerBound? x = some y → y ∈ t.toList
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
SheafOfModules.LocalGeneratorsData.mk : {C : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        {M : SheafOfModules R} →
          [inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] →
            [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] →
              (I : Type w) →
                (X : I → C) → J.CoversTop X → ((i : I) → (M.over (X i)).GeneratingSections) → M.LocalGeneratorsData
-- Mathlib.ModelTheory.Algebra.Field.Basic
_private.Mathlib.ModelTheory.Algebra.Field.Basic.0.FirstOrder.Field.FieldAxiom.toSentence.match_1.eq_8 : ∀ (motive : FirstOrder.Field.FieldAxiom → Sort u_1) (h_1 : Unit → motive FirstOrder.Field.FieldAxiom.addAssoc)
  (h_2 : Unit → motive FirstOrder.Field.FieldAxiom.zeroAdd)
  (h_3 : Unit → motive FirstOrder.Field.FieldAxiom.negAddCancel)
  (h_4 : Unit → motive FirstOrder.Field.FieldAxiom.mulAssoc) (h_5 : Unit → motive FirstOrder.Field.FieldAxiom.mulComm)
  (h_6 : Unit → motive FirstOrder.Field.FieldAxiom.oneMul) (h_7 : Unit → motive FirstOrder.Field.FieldAxiom.existsInv)
  (h_8 : Unit → motive FirstOrder.Field.FieldAxiom.leftDistrib)
  (h_9 : Unit → motive FirstOrder.Field.FieldAxiom.existsPairNE),
  (match FirstOrder.Field.FieldAxiom.leftDistrib with
    | FirstOrder.Field.FieldAxiom.addAssoc => h_1 ()
    | FirstOrder.Field.FieldAxiom.zeroAdd => h_2 ()
    | FirstOrder.Field.FieldAxiom.negAddCancel => h_3 ()
    | FirstOrder.Field.FieldAxiom.mulAssoc => h_4 ()
    | FirstOrder.Field.FieldAxiom.mulComm => h_5 ()
    | FirstOrder.Field.FieldAxiom.oneMul => h_6 ()
    | FirstOrder.Field.FieldAxiom.existsInv => h_7 ()
    | FirstOrder.Field.FieldAxiom.leftDistrib => h_8 ()
    | FirstOrder.Field.FieldAxiom.existsPairNE => h_9 ()) =
    h_8 ()
-- Std.Data.HashMap.Lemmas
Std.HashMap.mem_of_mem_keys : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, k ∈ m.keys → k ∈ m
-- Lean.Parser.Syntax
Lean.Parser.Command.elab_rules.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.NumberTheory.ModularForms.NormTrace
ModularForm.coe_norm : ∀ {𝒢 : Subgroup (GL (Fin 2) ℝ)} (ℋ : Subgroup (GL (Fin 2) ℝ)) {F : Type u_1} (f : F) [inst : FunLike F UpperHalfPlane ℂ]
  {k : ℤ} [inst_1 : 𝒢.IsFiniteRelIndex ℋ] [inst_2 : ℋ.HasDetPlusMinusOne] [inst_3 : ModularFormClass F 𝒢 k],
  ⇑(ModularForm.norm ℋ f) = ∏ q, SlashInvariantForm.quotientFunc f q
-- Mathlib.Topology.Gluing
/-- For each `i : J`, a bundled topological space `U i`  -/
TopCat.GlueData.MkCore.U : (self : TopCat.GlueData.MkCore) → self.J → TopCat
-- Mathlib.Analysis.Normed.Module.Convex
Filter.Eventually.segment_of_prod_nhdsWithin : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {s : Set E} {α : Type u_2} {f : Filter α}
  {x : E} {y z : α → E} {r : α → E → Prop},
  Filter.Tendsto y f (nhds x) →
    Filter.Tendsto z f (nhds x) →
      (∀ᶠ (p : α × E) in f ×ˢ nhdsWithin x s, r p.1 p.2) →
        (∀ᶠ (χ : α) in f, segment ℝ (y χ) (z χ) ⊆ s) → ∀ᶠ (χ : α) in f, ∀ v ∈ segment ℝ (y χ) (z χ), r χ v
-- Lean.Elab.BuiltinTerm
Lean.Elab.Term.elabDeclName : Lean.Elab.Term.TermElab
-- Lean.Meta.Sym.ExprPtr
Lean.Meta.Sym.ExprPtr.mk : Lean.Expr → Lean.Meta.Sym.ExprPtr
-- Mathlib.Geometry.Manifold.VectorBundle.Hom
/-- Consider a differentiable map `v : M → E₁` to a vector bundle, over a base map `b : M → B`, and
linear maps `ϕ m : E₁ (b m) → E₂ (b m)` depending smoothly on `m`.
One can apply `ϕ m` to `v m`, and the resulting map is differentiable.

We give here a version of this statement at a point.  -/
MDifferentiableAt.clm_bundle_apply : ∀ {𝕜 : Type u_1} {B : Type u_2} {F₁ : Type u_3} {F₂ : Type u_4} {M : Type u_6} [inst : NontriviallyNormedField 𝕜]
  {E₁ : B → Type u_7} [inst_1 : (x : B) → AddCommGroup (E₁ x)] [inst_2 : (x : B) → Module 𝕜 (E₁ x)]
  [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁] [inst_5 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
  [inst_6 : (x : B) → TopologicalSpace (E₁ x)] {E₂ : B → Type u_8} [inst_7 : (x : B) → AddCommGroup (E₂ x)]
  [inst_8 : (x : B) → Module 𝕜 (E₂ x)] [inst_9 : NormedAddCommGroup F₂] [inst_10 : NormedSpace 𝕜 F₂]
  [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [inst_12 : (x : B) → TopologicalSpace (E₂ x)] {EB : Type u_10}
  [inst_13 : NormedAddCommGroup EB] [inst_14 : NormedSpace 𝕜 EB] {HB : Type u_11} [inst_15 : TopologicalSpace HB]
  {IB : ModelWithCorners 𝕜 EB HB} [inst_16 : TopologicalSpace B] [inst_17 : ChartedSpace HB B] {EM : Type u_12}
  [inst_18 : NormedAddCommGroup EM] [inst_19 : NormedSpace 𝕜 EM] {HM : Type u_13} [inst_20 : TopologicalSpace HM]
  {IM : ModelWithCorners 𝕜 EM HM} [inst_21 : TopologicalSpace M] [inst_22 : ChartedSpace HM M]
  [inst_23 : FiberBundle F₁ E₁] [inst_24 : VectorBundle 𝕜 F₁ E₁] [inst_25 : FiberBundle F₂ E₂]
  [inst_26 : VectorBundle 𝕜 F₂ E₂] {b : M → B} {v : (x : M) → E₁ (b x)} {x : M}
  [inst_27 : ∀ (x : B), IsTopologicalAddGroup (E₂ x)] [inst_28 : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
  {ϕ : (x : M) → E₁ (b x) →L[𝕜] E₂ (b x)}, MDiffAt (T% ϕ) x → MDiffAt (T% v) x → (MDiffAt fun m => ⟨b m, ⋯⟩) x
-- Std.Time.Date.Basic
/-- Convert `Second.Offset` into `Day.Offset`.
 -/
Std.Time.Second.Offset.toDays : Std.Time.Second.Offset → Std.Time.Day.Offset
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.assoc : ∀ {B : Type u} [inst : Quiver B] {a b : B} {f g h i : CategoryTheory.FreeBicategory.Hom a b}
  (η : CategoryTheory.FreeBicategory.Hom₂ f g) (θ : CategoryTheory.FreeBicategory.Hom₂ g h)
  (ι : CategoryTheory.FreeBicategory.Hom₂ h i),
  CategoryTheory.FreeBicategory.Rel ((η.vcomp θ).vcomp ι) (η.vcomp (θ.vcomp ι))
-- Std.Data.ExtDHashMap.Basic
/-- Tries to retrieve the mapping for the given key, panicking if no such mapping is present.  -/
Std.ExtDHashMap.Const.get! : {α : Type u} →
  {x : BEq α} →
    {x_1 : Hashable α} →
      {β : Type v} → [EquivBEq α] → [LawfulHashable α] → [Inhabited β] → (Std.ExtDHashMap α fun x => β) → α → β
-- Aesop.RuleTac.Descr
Aesop.RuleTacDescr.ruleTac.sizeOf_spec : ∀ (decl : Lean.Name), sizeOf (Aesop.RuleTacDescr.ruleTac decl) = 1 + sizeOf decl
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.coproducts.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C),
  CategoryTheory.MorphismProperty.coproducts.{w, v, u} W = ⨆ J, W.colimitsOfShape (CategoryTheory.Discrete J)
-- Mathlib.Algebra.Opposites
MulOpposite.isRightCancelAdd_iff : ∀ {α : Type u_1} [inst : Add α], IsRightCancelAdd αᵐᵒᵖ ↔ IsRightCancelAdd α
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- The width of the BitVec variable.
 -/
Std.Tactic.BVDecide.BVBit.w : Std.Tactic.BVDecide.BVBit → ℕ
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.coe_eq_zero : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M} {p : Submodule R M}
  {x : ↥p}, ↑x = 0 ↔ x = 0
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
HasFDerivWithinAt.eventually_ne : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {x : E} {s : Set E} {c : F},
  HasFDerivWithinAt f f' s x → (∃ C, AntilipschitzWith C ⇑f') → ∀ᶠ (z : E) in nhdsWithin x (s \ {x}), f z ≠ c
-- Mathlib.Algebra.Algebra.Unitization
Unitization.fst_mul : ∀ {R : Type u_1} {A : Type u_2} [inst : Mul R] [inst_1 : Add A] [inst_2 : Mul A] [inst_3 : SMul R A]
  (x₁ x₂ : Unitization R A), (x₁ * x₂).toProd.1 = x₁.toProd.1 * x₂.toProd.1
-- Mathlib.Order.Category.LinOrd
LinOrd.hom_ext_iff : ∀ {X Y : LinOrd} {f g : X ⟶ Y}, f = g ↔ LinOrd.Hom.hom f = LinOrd.Hom.hom g
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Λ'.read.sizeOf_spec : ∀ (f : Option Turing.PartrecToTM2.Γ' → Turing.PartrecToTM2.Λ'), sizeOf (Turing.PartrecToTM2.Λ'.read f) = 1
-- Mathlib.RingTheory.Multiplicity
Nat.finiteMultiplicity_iff : ∀ {a b : ℕ}, FiniteMultiplicity a b ↔ a ≠ 1 ∧ 0 < b
-- Lean.Environment
Lean.Kernel.Exception.exprTypeMismatch.inj : ∀ {env : Lean.Kernel.Environment} {lctx : Lean.LocalContext} {expr expectedType : Lean.Expr}
  {env_1 : Lean.Kernel.Environment} {lctx_1 : Lean.LocalContext} {expr_1 expectedType_1 : Lean.Expr},
  Lean.Kernel.Exception.exprTypeMismatch env lctx expr expectedType =
      Lean.Kernel.Exception.exprTypeMismatch env_1 lctx_1 expr_1 expectedType_1 →
    env = env_1 ∧ lctx = lctx_1 ∧ expr = expr_1 ∧ expectedType = expectedType_1
-- Mathlib.Algebra.Homology.SpectralObject.Differentials
CategoryTheory.Abelian.SpectralObject.cyclesMap_Ψ_exact : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₁₂ : i ⟶ k)
  (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) (f₂₃ : j ⟶ l)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.cyclesMap_Ψ_exact._auto_1),
  { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
      f := X.cyclesMap f₁₂ f₃ f₂ f₃ (CategoryTheory.ComposableArrows.threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀,
      g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ }.Exact
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
/-- The scheme-theoretic image of a morphism.  -/
AlgebraicGeometry.Scheme.Hom.image : {X Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → AlgebraicGeometry.Scheme
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.skeletonEquivalence_counitIso : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C],
  (CategoryTheory.skeletonEquivalence C).counitIso =
    CategoryTheory.NatIso.ofComponents CategoryTheory.fromSkeletonToSkeletonIso ⋯
-- Mathlib.Algebra.Ring.Defs
/-- Multiplication is left distributive over addition  -/
Semiring.left_distrib : ∀ {α : Type u} [self : Semiring α] (a b c : α), a * (b + c) = a * b + a * c
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- The top `AddSubmonoid` is isomorphic to the `AddMonoid`.  -/
AddSubmonoid.topEquiv : {M : Type u_5} → [inst : AddZeroClass M] → ↥⊤ ≃+ M
-- Mathlib.Order.Interval.Set.ProjIcc
Set.projIic.eq_1 : ∀ {α : Type u_1} [inst : LinearOrder α] (b x : α), Set.projIic b x = ⟨min b x, ⋯⟩
-- Mathlib.MeasureTheory.Group.AEStabilizer
MeasureTheory.inv_smul_ae_eq_self : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {x : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] {x_1 : G} {s : Set α},
  x_1 • s =ᵐ[μ] s → x_1⁻¹ • s =ᵐ[μ] s
-- Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
AlgebraicGeometry.Scheme.IdealSheafData.subschemeMap_subschemeι_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (J : Y.IdealSheafData) (f : X ⟶ Y) (H : J ≤ I.map f)
  {Z : AlgebraicGeometry.Scheme} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (I.subschemeMap J f H) (CategoryTheory.CategoryStruct.comp J.subschemeι h) =
    CategoryTheory.CategoryStruct.comp I.subschemeι (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.RingTheory.SimpleRing.Basic
IsSimpleRing.instMulOpposite : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] [IsSimpleRing R], IsSimpleRing Rᵐᵒᵖ
-- Mathlib.Topology.Algebra.Monoid
AddSubsemigroup.top_closure_add_self_subset : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddSemigroup M] [SeparatelyContinuousAdd M]
  (s : AddSubsemigroup M), closure ↑s + closure ↑s ⊆ closure ↑s
-- Mathlib.Order.Heyting.Hom
HeytingHom.coe_id : ∀ (α : Type u_2) [inst : HeytingAlgebra α], ⇑(HeytingHom.id α) = id
-- Mathlib.GroupTheory.Commensurable
/-- Equivalence of `K / (H ⊓ K)` with `gKg⁻¹/ (gHg⁻¹ ⊓ gKg⁻¹)`  -/
Subgroup.quotConjEquiv : {G : Type u_1} →
  [inst : Group G] → (H K : Subgroup G) → (g : ConjAct G) → ↥K ⧸ H.subgroupOf K ≃ ↥(g • K) ⧸ (g • H).subgroupOf (g • K)
-- Mathlib.Topology.Algebra.Algebra
/-- `Prod.snd` as a `ContinuousAlgHom`.  -/
ContinuousAlgHom.snd : (R : Type u_1) →
  [inst : CommSemiring R] →
    (A : Type u_2) →
      [inst_1 : Semiring A] →
        [inst_2 : TopologicalSpace A] →
          (B : Type u_3) →
            [inst_3 : Semiring B] →
              [inst_4 : TopologicalSpace B] → [inst_5 : Algebra R A] → [inst_6 : Algebra R B] → A × B →A[R] B
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.liftOn_div : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] {P : Sort v} (p q : Polynomial K)
  (f : Polynomial K → Polynomial K → P),
  (∀ (p : Polynomial K), f p 0 = f 0 1) →
    ∀ (H' : ∀ {p q p' q' : Polynomial K}, q ≠ 0 → q' ≠ 0 → q' * p = q * p' → f p q = f p' q')
      (H :
        optParam
          (∀ {p q p' q' : Polynomial K},
            q ∈ nonZeroDivisors (Polynomial K) →
              q' ∈ nonZeroDivisors (Polynomial K) → q' * p = q * p' → f p q = f p' q')
          ⋯),
      ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q).liftOn f H = f p q
-- Mathlib.Algebra.Order.Module.Defs
strictMono_smul_left_of_pos : ∀ {α : Type u_1} {β : Type u_2} {a : α} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β] [inst_3 : Zero α]
  [PosSMulStrictMono α β], 0 < a → StrictMono fun x => a • x
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.FunctionTheorems : Type
-- Mathlib.AlgebraicTopology.DoldKan.Projections
AlgebraicTopology.DoldKan.P_succ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} (q : ℕ),
  AlgebraicTopology.DoldKan.P (q + 1) =
    CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.P q)
      (CategoryTheory.CategoryStruct.id (AlgebraicTopology.AlternatingFaceMapComplex.obj X) +
        AlgebraicTopology.DoldKan.Hσ q)
-- Mathlib.Analysis.Complex.UpperHalfPlane.Topology
UpperHalfPlane.instLocallyCompactSpace : LocallyCompactSpace UpperHalfPlane
-- Mathlib.LinearAlgebra.Determinant
Module.Basis.det_isEmpty : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_4}
  [inst_3 : DecidableEq ι] [inst_4 : Fintype ι] (e : Module.Basis ι R M) [inst_5 : IsEmpty ι],
  e.det = AlternatingMap.constOfIsEmpty R M ι 1
-- Mathlib.Data.Seq.Computation
Computation.length_pure : ∀ {α : Type u} (a : α), (Computation.pure a).length = 0
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiff.add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {G : Type u_4} [inst_4 : Add G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] {E' : Type u_5}
  [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_9 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [inst_10 : TopologicalSpace M] [inst_11 : ChartedSpace H' M]
  [ContMDiffAdd I n G] {f g : M → G}, ContMDiff I' I n f → ContMDiff I' I n g → ContMDiff I' I n (f + g)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.insertIfNew.eq_1 : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t : Std.ExtDTreeMap α β cmp) (a : α)
  (b : β a), t.insertIfNew a b = Std.ExtDTreeMap.lift (fun m => Std.ExtDTreeMap.mk (m.insertIfNew a b)) ⋯ t
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
AddOpposite.op_finsuppProd : ∀ {ι : Type u_16} {M : Type u_17} {N : Type u_18} [inst : CommMonoid M] [inst_1 : Zero N] (f : ι →₀ N) (g : ι → N → M),
  AddOpposite.op (f.prod g) = f.prod fun i n => AddOpposite.op (g i n)
-- Lean.Elab.Do.Basic
/-- The continuation to elaborate the `rest` of the block. It assumes that the result of the `do`
block is bound to `resultName` with the correct type (that is, `resultType`, potentially refined
by a dependent `match`).
 -/
Lean.Elab.Do.DoElemCont.k : Lean.Elab.Do.DoElemCont → Lean.Elab.Do.DoElabM Lean.Expr
-- Mathlib.Order.RelIso.Basic
RelEmbedding.preimage_apply : ∀ {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : β → β → Prop) (a : α), (RelEmbedding.preimage f s) a = f a
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.nonempty_coe : ∀ {α : Type u_2} [inst : TopologicalSpace α] {U : TopologicalSpace.Opens α}, (↑U).Nonempty ↔ ∃ x, x ∈ U
-- Mathlib.Algebra.Homology.Embedding.IsSupported
HomologicalComplex.isZero_iff_isStrictlySupported_and_isStrictlySupportedOutside : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c'),
  CategoryTheory.Limits.IsZero K ↔ K.IsStrictlySupported e ∧ K.IsStrictlySupportedOutside e
-- Mathlib.RingTheory.FiniteType
/-- **Alias** of `RingHom.FiniteType.of_finite`. -/
RingHom.Finite.to_finiteType : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] {f : A →+* B}, f.Finite → f.FiniteType
-- Mathlib.CategoryTheory.Galois.Prorepresentability
_private.Mathlib.CategoryTheory.Galois.Prorepresentability.0.CategoryTheory.PreGaloisCategory.termF' : Lean.ParserDescr
-- Lean.Meta.RecursorInfo
Lean.Meta.RecursorInfo.depElim : Lean.Meta.RecursorInfo → Bool
-- Init.Grind.Ring.CommSemiringAdapter
_private.Init.Grind.Ring.CommSemiringAdapter.0.Lean.Grind.CommRing.Expr.toPolyS.match_4.eq_7 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (a b : Lean.Grind.CommRing.Expr)
  (h_1 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.num n))
  (h_2 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_3 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_4 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b))
  (h_5 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k))
  (h_6 : (n : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast n))
  (h_7 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b)) (h_8 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_9 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k)),
  (match a.sub b with
    | Lean.Grind.CommRing.Expr.num n => h_1 n
    | Lean.Grind.CommRing.Expr.var x => h_2 x
    | a.add b => h_3 a b
    | a.mul b => h_4 a b
    | a.pow k => h_5 a k
    | Lean.Grind.CommRing.Expr.natCast n => h_6 n
    | a.sub b => h_7 a b
    | a.neg => h_8 a
    | Lean.Grind.CommRing.Expr.intCast k => h_9 k) =
    h_7 a b
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : CategoryTheory.IsTriangulated C] (a b : EInt),
  t.eTruncLTGEIsoGELT a b = t.eTruncLTGEIsoGELT a b
-- Mathlib.AlgebraicTopology.SimplexCategory.Defs
/-- The inclusion of `Truncated n` into `Truncated m` when `n ≤ m`.  -/
SimplexCategory.Truncated.incl : (n m : ℕ) →
  autoParam (n ≤ m) SimplexCategory.Truncated.incl._auto_1 →
    CategoryTheory.Functor (SimplexCategory.Truncated n) (SimplexCategory.Truncated m)
-- Mathlib.ModelTheory.Definability
FirstOrder.Language.DefinableSet.mem_top : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {A : Set M} {α : Type u₁} {x : α → M}, x ∈ ⊤