mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
I✝ I : Ideal R
inst✝ : I.IsTwoSided
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
𝔪_mem : 𝔪 ∈ {J | I ≤ J ∧ J.IsMaximal}
r𝔪 : r ∉ 𝔪
𝔪₀ : Ideal R := Submodule.comap (DistribSMul.toLinearMap R R (MulOpposite.op r)) 𝔪
I𝔪₀ : I ≤ 𝔪₀
J : Ideal R
b : R
𝔪₀J : 𝔪₀ ≤ J
b𝔪₀ : b ∉ 𝔪₀
bJ : b ∈ J
K : Ideal R := span {b * r} ⊔ 𝔪
s y : R
y𝔪 : y ∈ 𝔪
sbyr : y = r - s * (b * r)
⊢ 1 - s * b ∈ 𝔪₀

Tactic:
sbyr,

Goal state after:
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
I✝ I : Ideal R
inst✝ : I.IsTwoSided
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
𝔪_mem : 𝔪 ∈ {J | I ≤ J ∧ J.IsMaximal}
r𝔪 : r ∉ 𝔪
𝔪₀ : Ideal R := Submodule.comap (DistribSMul.toLinearMap R R (MulOpposite.op r)) 𝔪
I𝔪₀ : I ≤ 𝔪₀
J : Ideal R
b : R
𝔪₀J : 𝔪₀ ≤ J
b𝔪₀ : b ∉ 𝔪₀
bJ : b ∈ J
K : Ideal R := span {b * r} ⊔ 𝔪
s y : R
y𝔪 : r - s * (b * r) ∈ 𝔪
sbyr : y = r - s * (b * r)
⊢ 1 - s * b ∈ 𝔪₀
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
I✝ I : Ideal R
inst✝ : I.IsTwoSided
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
𝔪_mem : 𝔪 ∈ {J | I ≤ J ∧ J.IsMaximal}
r𝔪 : r ∉ 𝔪
𝔪₀ : Ideal R := Submodule.comap (DistribSMul.toLinearMap R R (MulOpposite.op r)) 𝔪
I𝔪₀ : I ≤ 𝔪₀
J : Ideal R
b : R
𝔪₀J : 𝔪₀ ≤ J
b𝔪₀ : b ∉ 𝔪₀
bJ : b ∈ J
K : Ideal R := span {b * r} ⊔ 𝔪
s y : R
y𝔪 : r - s * b * r ∈ 𝔪
sbyr : y = r - s * (b * r)
⊢ 1 - s * b ∈ 𝔪₀

Tactic:
simp [𝔪₀, sub_mul, y𝔪]

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
hd : d ≤ 0
⊢ selfZPow x B d * selfZPow x B (-d) = 1

Tactic:
rw [selfZPow_of_nonpos x B hd, selfZPow_of_nonneg, ← map_pow, Int.natAbs_neg,
      Submonoid.pow_apply, IsLocalization.mk'_spec, map_one]
    apply nonneg_of_neg_nonpos
    rwa [neg_neg]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
M X Y : C
inst✝ : MonObj M
e : M ≅ X
⊢ X ◁ (η ≫ e.hom) ≫ (e.inv ⊗ₘ e.inv) ≫ μ ≫ e.hom = (ρ_ X).hom

Tactic:
rw [← cancel_epi (ρ_ X).inv]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
M X Y : C
inst✝ : MonObj M
e : M ≅ X
⊢ (ρ_ X).inv ≫ X ◁ (η ≫ e.hom) ≫ (e.inv ⊗ₘ e.inv) ≫ μ ≫ e.hom = (ρ_ X).inv ≫ (ρ_ X).hom
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
M X Y : C
inst✝ : MonObj M
e : M ≅ X
⊢ X ◁ (η ≫ e.hom) ≫ (e.inv ⊗ₘ e.inv) ≫ μ ≫ e.hom = (ρ_ X).hom

Tactic:
by
    rw [← cancel_epi (ρ_ X).inv]
    simp only [MonoidalCategory.whiskerLeft_comp, tensorHom_def', Category.assoc,
      whiskerLeft_hom_inv_assoc, Iso.inv_hom_id]
    simp [← tensorHom_def'_assoc, rightUnitor_inv_comp_tensorHom_assoc]

Goal state after:
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
b : Basis ι R M
i : ι
⊢ (ofIsLocalizedModule Rₛ S f b) i = f (b i)

Tactic:
by
  rw [ofIsLocalizedModule, coe_mk, Function.comp_apply]

Goal state after:
Module: Mathlib.RingTheory.Localization.BaseChange

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M₁ : Type u_5
M₂ : Type u_6
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
inst✝³ : Module A M₁
inst✝² : Module A M₂
inst✝¹ : IsScalarTower R A M₁
inst✝ : IsScalarTower R A M₂
x✝¹ : M₁
x✝ : M₂
r : R
s : ↥S
⊢ (mk' A r s • x✝¹) ⊗ₜ[R] x✝ = x✝¹ ⊗ₜ[R] (mk' A r s • x✝)

Tactic:
rw [← (map_units A s).smul_left_cancel]

Goal state after:
R : Type u_1
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M₁ : Type u_5
M₂ : Type u_6
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
inst✝³ : Module A M₁
inst✝² : Module A M₂
inst✝¹ : IsScalarTower R A M₁
inst✝ : IsScalarTower R A M₂
x✝¹ : M₁
x✝ : M₂
r : R
s : ↥S
⊢ (algebraMap R A) ↑s • (mk' A r s • x✝¹) ⊗ₜ[R] x✝ = (algebraMap R A) ↑s • x✝¹ ⊗ₜ[R] (mk' A r s • x✝)
Module: Mathlib.CategoryTheory.Monad.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G : Comonad C
M N : Monad C
f : M.toFunctor ≅ N.toFunctor
f_η : ∀ (X : C), M.η.app X ≫ f.hom.app X = N.η.app X
f_μ : ∀ (X : C), M.μ.app X ≫ f.hom.app X = (M.map (f.hom.app X) ≫ f.hom.app (N.obj X)) ≫ N.μ.app X
X : C
⊢ N.μ.app X ≫ f.inv.app X = (N.map (f.inv.app X) ≫ f.inv.app (M.obj X)) ≫ M.μ.app X

Tactic:
by
        rw [← NatIso.cancel_natIso_hom_right f]
        simp only [NatTrans.naturality, Iso.inv_hom_id_app, assoc, comp_id, f_μ,
          NatTrans.naturality_assoc, Iso.inv_hom_id_app_assoc, ← Functor.map_comp_assoc]
        simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case property.left
R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : PushoutCocone (ofHom (algebraMap R A)) (ofHom (algebraMap R B))
this✝ : Algebra R ↑s.pt := ⋯
f' : A →ₐ[R] ↑s.pt := ⋯
g' : B →ₐ[R] ↑s.pt := ⋯
this : Algebra R ↑(pushoutCocone R A B).pt := ⋯
⊢ ofHom Algebra.TensorProduct.includeLeftRingHom ≫ ofHom (Algebra.TensorProduct.productMap f' g').toRingHom = s.inl

Tactic:
ext x
      exact Algebra.TensorProduct.productMap_left_apply (A := A) _ _ x

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
r : J → J → Prop
hr : _root_.Equivalence r
h : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), r j₁ j₂
⊢ ∀ (j₁ j₂ : J), r j₁ j₂

Tactic:
intro j₁ j₂
  have z : ∀ j : J, r j₁ j :=
    induct_on_objects {k | r j₁ k} (hr.1 j₁)
      fun f => ⟨fun t => hr.3 t (h f), fun t => hr.3 t (hr.2 (h f))⟩
  exact z j₂

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Products

Goal state before:
pp: ⊢ binaryProductFunctor ≅ prod.functor

Tactic:
refine NatIso.ofComponents (fun X => ?_) (fun _ => ?_)
  · refine NatIso.ofComponents (fun Y => ?_) (fun _ => ?_)
    · exact ((limit.isLimit _).conePointUniqueUpToIso (binaryProductLimit X Y)).symm
    · apply Limits.prod.hom_ext <;> simp <;> rfl
  · ext : 2
    apply Limits.prod.hom_ext <;> simp <;> rfl

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P Q : ObjectProperty C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} Q
h : P ≤ Q
R : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} R
hR : Q ≤ R.isoClosure
⊢ ∃ Q, ∃ (_ : ObjectProperty.Small.{w, v, u} Q), P ≤ Q.isoClosure

Tactic:
exact ⟨R, inferInstance, h.trans hR⟩

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
⊢ EssentiallySmall.{w, v, u} C ↔ ObjectProperty.EssentiallySmall.{w, v, u} ⊤

Tactic:
rw [← exists_equivalence_iff_of_locallySmall]
  exact ⟨fun _ ↦ ⟨_, _, ⟨equivSmallModel.{w} C⟩⟩,
    fun ⟨C₀, _, ⟨e⟩⟩ ↦ ⟨C₀, inferInstance, ⟨e⟩⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Type w
⊢ ∀ (X : Grothendieck (G ⋙ typeToCat)),
    (grothendieckTypeToCatFunctor G).map
          ((NatIso.ofComponents
                  (fun X ↦
                    casesOn X fun base fiber ↦
                      Discrete.casesOn fiber fun as ↦
                        Iso.refl ((𝟭 (Grothendieck (G ⋙ typeToCat))).obj { base := base, fiber := { as := as } }))
                  ⋯).hom.app
            X) ≫
        (NatIso.ofComponents
                (fun X ↦
                  Sigma.casesOn (motive := fun t ↦
                    X = t →
                      ((grothendieckTypeToCatInverse G ⋙ grothendieckTypeToCatFunctor G).obj X ≅ (𝟭 G.Elements).obj X))
                    X
                    (fun fst snd h ↦
                      ⋯ ▸ Iso.refl ((grothendieckTypeToCatInverse G ⋙ grothendieckTypeToCatFunctor G).obj ⟨fst, snd⟩))
                    ⋯)
                ⋯).hom.app
          ((grothendieckTypeToCatFunctor G).obj X) =
      𝟙 ((grothendieckTypeToCatFunctor G).obj X)

Tactic:
rintro ⟨_, ⟨⟩⟩
    simp
    rfl

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case hy
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ⇑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker f.toRingHom
RX : Type (max w₁ 0) := ⋯
AX : Type (max w₂ 0) := ⋯
t : Finset A
ht : adjoin R ↑t = ⊤
t' : ↥t → MvPolynomial (Fin n) R
ht' : ∀ (i : ↥t), f (t' i) = (algebraMap A B) ↑i
ht'' : adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : ↥t → AX := ⋯
s₀✝ : Set (MvPolynomial (Fin n) A) := ⋯
I : Ideal (MvPolynomial (Fin n) A) := ⋯
leI :
  Ideal.span (⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ⋯
this : x ∈ adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
p₁ : MvPolynomial (Fin n) R
q₁ : MvPolynomial (Fin n) A
hq₁ : q₁ ∈ (Ideal.span s₀).toAddSubmonoid
hx✝ : (MvPolynomial.map (algebraMap R A)) p₁ + q₁ ∈ adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
h₁ :
  (MvPolynomial.map (algebraMap R A)) p₁ + q₁ ∈
    (MvPolynomial.map (algebraMap R A)).range.toAddSubmonoid ⊔ (Ideal.span s₀).toAddSubmonoid
p₂ : MvPolynomial (Fin n) R
q₂ : MvPolynomial (Fin n) A
hq₂ : q₂ ∈ (Ideal.span s₀).toAddSubmonoid
hy✝ : (MvPolynomial.map (algebraMap R A)) p₂ + q₂ ∈ adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
h₂ :
  (MvPolynomial.map (algebraMap R A)) p₂ + q₂ ∈
    (MvPolynomial.map (algebraMap R A)).range.toAddSubmonoid ⊔ (Ideal.span s₀).toAddSubmonoid
⊢ (MvPolynomial.map (algebraMap R A)) p₁ * q₂ + q₁ * ((MvPolynomial.map (algebraMap R A)) p₂ + q₂) ∈
    (Ideal.span s₀).toAddSubmonoid

Tactic:
· refine add_mem (Ideal.mul_mem_left _ _ hq₂) (Ideal.mul_mem_right _ _ hq₁)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: case trans
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y z : (X : C) × (d ⟶ F.obj X)
a✝¹ : Relation.EqvGen (F ⋙ coyoneda.obj (op d)).ColimitTypeRel x y
a✝ : Relation.EqvGen (F ⋙ coyoneda.obj (op d)).ColimitTypeRel y z
ih₁ : Zigzag (StructuredArrow.mk x.snd) (StructuredArrow.mk y.snd)
ih₂ : Zigzag (StructuredArrow.mk y.snd) (StructuredArrow.mk z.snd)
⊢ Zigzag (StructuredArrow.mk x.snd) (StructuredArrow.mk z.snd)

Tactic:
| trans x y z _ _ ih₁ ih₂ =>

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f
inst✝ : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ⇑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker f'.toRingHom
RXn : Type (max w₁ 0) := MvPolynomial (Fin n) R
RXm : Type (max w₁ 0) := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), f' (g i) = f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), f (h i) = f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
⊢ (RingHom.ker f.toRingHom).FG

Tactic:
let g' : Fin n → RXn := fun i => X i - aeval_h (g i)

Goal state after:
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f
inst✝ : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ⇑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker f'.toRingHom
RXn : Type (max w₁ 0) := MvPolynomial (Fin n) R
RXm : Type (max w₁ 0) := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), f' (g i) = f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), f (h i) = f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i ↦ MvPolynomial.X i - aeval_h (g i)
⊢ (RingHom.ker f.toRingHom).FG
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y : C
f g : X ⟶ Y
c : Cofork f g
⊢ IsColimit c ≃ IsLimit c.op

Tactic:
apply equivOfSubsingletonOfSubsingleton
  · intro h
    exact (IsLimit.postcomposeHomEquiv _ _).invFun ((IsLimit.whiskerEquivalenceEquiv _).toFun h.op)
  · intro h
    exact (IsColimit.equivIsoColimit c.opUnopIso).toFun (((IsLimit.postcomposeHomEquiv _ _).invFun
      ((IsLimit.whiskerEquivalenceEquiv walkingParallelPairOpEquiv.symm).toFun h)).unop)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : HasPushout f f
h : IsColimit (Cofork.ofπ f.unop ⋯)
⊢ (Iso.refl (Opposite.op (Opposite.unop Y))).hom ≫ pushout.inr f f =
    (pullback.snd f.unop f.unop).op ≫ (pushoutIsoOpPullback f f).symm.hom

Tactic:
rw [Iso.symm_hom, ← Quiver.Hom.op_unop (pushoutIsoOpPullback f f).inv, ← op_comp,
        pushoutIsoOpPullback_inv_snd, Quiver.Hom.op_unop, Iso.refl_hom, Category.id_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
c : C
hc : IsTerminal c
c' : C
this : Inhabited (StructuredArrow c' (fromPUnit c)) := { default := StructuredArrow.mk (hc.from c') }
⊢ IsConnected (StructuredArrow c' (fromPUnit c))

Tactic:
let : Subsingleton (StructuredArrow c' (fromPUnit c)) :=
      ⟨fun i j ↦ StructuredArrow.obj_ext _ _ (by cat_disch) (hc.hom_ext _ _)⟩

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
c : C
hc : IsTerminal c
c' : C
this✝ : Inhabited (StructuredArrow c' (fromPUnit c)) := { default := StructuredArrow.mk (hc.from c') }
this : Subsingleton (StructuredArrow c' (fromPUnit c)) :=
  {
    allEq := fun i j ↦
      StructuredArrow.obj_ext i j (Subsingleton.elim i.right j.right)
        (IsTerminal.hom_ext hc (i.hom ≫ (fromPUnit c).map (eqToHom (Subsingleton.elim i.right j.right))) j.hom) }
⊢ IsConnected (StructuredArrow c' (fromPUnit c))
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
c : C
hc : IsInitial c
c' : C
⊢ IsConnected (CostructuredArrow (fromPUnit c) c')

Tactic:
let : Inhabited (CostructuredArrow (fromPUnit c) c') := ⟨.mk (Y := default) (hc.to c')⟩

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
c : C
hc : IsInitial c
c' : C
this : Inhabited (CostructuredArrow (fromPUnit c) c') := { default := CostructuredArrow.mk (hc.to c') }
⊢ IsConnected (CostructuredArrow (fromPUnit c) c')
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
⊢ IsLimit (Fork.ofι g ⋯)

Tactic:
by
    apply Fork.IsLimit.mk' _ _
    intro s
    have l₁ : (Fork.ι s ≫ k) ≫ hr.left = (Fork.ι s ≫ k) ≫ hr.right := by
      rw [Category.assoc, s.condition, Category.assoc]
    obtain ⟨l, hl⟩ := Fork.IsLimit.lift' hr.isLimit _ l₁
    obtain ⟨p, _, hp₂⟩ := PullbackCone.IsLimit.lift' t _ _ hl
    refine ⟨p, hp₂, ?_⟩
    intro m w
    have z : m ≫ g = p ≫ g := w.trans hp₂.symm
    apply t.hom_ext
    have := hr.mono
    apply (PullbackCone.mk f g comm).equalizer_ext
    · simp only [PullbackCone.mk_π_app, ← cancel_mono h]
      grind [Fork.ofι, PullbackCone.mk]
    · exact z

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
T : C ⥤ D
inst✝ : T.Initial
S : D ⥤ E
X : E
⊢ (pre T S X).Initial

Tactic:
by
  refine ⟨fun f => ?_⟩
  rw [isConnected_iff_of_equivalence (CostructuredArrow.preEquivalence T f)]
  exact Initial.out f.left

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
⊢ { l // (Cofork.ofπ h ⋯).π ≫ l = s.π ∧ ∀ {m : (Cofork.ofπ h ⋯).pt ⟶ s.pt}, (Cofork.ofπ h ⋯).π ≫ m = s.π → m = l }

Tactic:
have l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π := by
      rw [← Category.assoc, ← Category.assoc, s.condition]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
⊢ { l // (Cofork.ofπ h ⋯).π ≫ l = s.π ∧ ∀ {m : (Cofork.ofπ h ⋯).pt ⟶ s.pt}, (Cofork.ofπ h ⋯).π ≫ m = s.π → m = l }
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
f : R →+* S
r : R
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
e₁ : R' ≃+* Localization.Away r := (IsLocalization.algEquiv (Submonoid.powers r) R' (Localization.Away r)).toRingEquiv
e₂ : Localization.Away (f r) ≃+* S' :=
  (IsLocalization.algEquiv (Submonoid.powers (f r)) (Localization.Away (f r)) S').toRingEquiv
⊢ Submonoid.powers r ≤ Submonoid.comap f (Submonoid.powers (f r))

Tactic:
rintro x ⟨n, rfl⟩; use n; simp

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Convolution

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
ι : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalSemiring A
inst✝⁵ : Module R A
inst✝⁴ : SMulCommClass R A A
inst✝³ : IsScalarTower R A A
inst✝² : AddCommMonoid C
inst✝¹ : Module R C
inst✝ : Coalgebra R C
f g h : WithConv (C →ₗ[R] A)
⊢ (mul' R A ∘ₗ rTensor A (mul' R A)) ∘ₗ
      (((f.ofConv ⊗ₘ g.ofConv) ⊗ₘ h.ofConv) ∘ₗ ↑(TensorProduct.assoc R C C C).symm) ∘ₗ lTensor C δ ∘ₗ δ =
    (mul' R A ∘ₗ rTensor A (mul' R A) ∘ₗ ↑(TensorProduct.assoc R A A A).symm) ∘ₗ
      (f.ofConv ⊗ₘ (g.ofConv ⊗ₘ h.ofConv)) ∘ₗ lTensor C δ ∘ₗ δ

Tactic:
simp only [map_map_comp_assoc_symm_eq, comp_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
A B : C
inst✝² : GrpObj A
inst✝¹ : GrpObj B
f : A ⟶ B
inst✝ : IsMonHom f
this : (lift (𝟙 A) ι ≫ μ) ≫ f = (toUnit A ≫ η) ≫ f
⊢ lift f (ι ≫ f) ≫ μ = toUnit A ≫ η

Tactic:
rwa [assoc, IsMonHom.mul_hom, assoc, IsMonHom.one_hom, lift_map_assoc, id_comp] at this

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
A B : C
inst✝² : GrpObj A
inst✝¹ : GrpObj B
f : A ⟶ B
inst✝ : IsMonHom f
this : (lift ι (𝟙 A) ≫ μ) ≫ f = (toUnit A ≫ η) ≫ f
⊢ lift (ι ≫ f) f ≫ μ = toUnit A ≫ η

Tactic:
rwa [assoc, IsMonHom.mul_hom, assoc, IsMonHom.one_hom, lift_map_assoc, id_comp] at this

Goal state after:
Module: Mathlib.Data.W.Cardinal

Goal state before:
pp: case mk
α : Type u
β : α → Type v
γ : Type (max u v)
hκ : (sum fun a ↦ #γ ^ lift.{u, v} #(β a)) ≤ #γ
⊢ #(WType β) ≤ #γ

Tactic:
← lift_umax.{v, u}

Goal state after:
case mk
α : Type u
β : α → Type v
γ : Type (max u v)
hκ : (sum fun a ↦ #γ ^ lift.{max u v, v} #(β a)) ≤ #γ
⊢ #(WType β) ≤ #γ
Module: Mathlib.LinearAlgebra.Coevaluation

Goal state before:
pp: K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (∑ x, if x = j then 1 ⊗ₜ[K] (Basis.ofVectorSpace K V).coord x else 0) = 1 ⊗ₜ[K] (Basis.ofVectorSpace K V).coord j

Tactic:
rw [Finset.sum_ite_eq']

Goal state after:
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (if j ∈ Finset.univ then 1 ⊗ₜ[K] (Basis.ofVectorSpace K V).coord j else 0) = 1 ⊗ₜ[K] (Basis.ofVectorSpace K V).coord j
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsRefl
⊢ B.ker = ⊥ ↔ B.flip.ker = ⊥

Tactic:
ker_flip

Goal state after:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsRefl
⊢ B.ker = ⊥ ↔ B.ker = ⊥

R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsRefl
⊢ B.IsRefl
Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryProducts C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
K : WalkingParallelPair ⥤ C
c : Cone (K ⋙ G)
j : WalkingParallelPair
⊢ (pullback.lift (c.π.app WalkingParallelPair.zero) (c.π.app WalkingParallelPair.zero) ⋯ ≫
        (PreservesPullback.iso G (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left))
            (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))).inv) ≫
      (G.mapCone (equalizerCone K)).π.app j =
    c.π.app j

Tactic:
rcases j with (_ | _) <;>
            simp only [Category.comp_id, PreservesPullback.iso_inv_fst, Cone.ofFork_π, G.map_comp,
              PreservesPullback.iso_inv_fst_assoc, Functor.mapCone_π_app, eqToHom_refl,
              Category.assoc, Fork.ofι_π_app, pullback.lift_fst, pullback.lift_fst_assoc]
          exact (c.π.naturality WalkingParallelPairHom.left).symm.trans (Category.id_comp _)

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K : Type uK
V : Type uV
inst✝³ : CommSemiring K
inst✝² : AddCommMonoid V
inst✝¹ : Module K V
inst✝ : Projective K V
⊢ Nontrivial (Dual K V) ↔ Nontrivial V

Tactic:
contrapose!; exact subsingleton_dual_iff K

Goal state after: