mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: case neg
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b : R
ha : a ≠ 0
h : ∀ (p : R), Prime p → emultiplicity p a ≤ emultiplicity p b
hb : ¬b = 0
this : StrongNormalizationMonoid R := UniqueFactorizationMonoid.strongNormalizationMonoid
q : R
⊢ Multiset.count q (normalizedFactors a) ≤ Multiset.count q (normalizedFactors b)

Tactic:
by_cases hq : q ∈ normalizedFactors a

Goal state after:
case pos
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b : R
ha : a ≠ 0
h : ∀ (p : R), Prime p → emultiplicity p a ≤ emultiplicity p b
hb : ¬b = 0
this : StrongNormalizationMonoid R := UniqueFactorizationMonoid.strongNormalizationMonoid
q : R
hq : q ∈ normalizedFactors a
⊢ Multiset.count q (normalizedFactors a) ≤ Multiset.count q (normalizedFactors b)

case neg
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b : R
ha : a ≠ 0
h : ∀ (p : R), Prime p → emultiplicity p a ≤ emultiplicity p b
hb : ¬b = 0
this : StrongNormalizationMonoid R := UniqueFactorizationMonoid.strongNormalizationMonoid
q : R
hq : q ∉ normalizedFactors a
⊢ Multiset.count q (normalizedFactors a) ≤ Multiset.count q (normalizedFactors b)
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case refine_3
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
x y : R
inst✝¹ : Away x S
inst✝ : Away ((algebraMap R S) y) T
a b : R
h : (algebraMap R T) a = (algebraMap R T) b
⊢ ∃ n, (y * x) ^ n * a = (y * x) ^ n * b

Tactic:
IsScalarTower.algebraMap_apply R S T

Goal state after:
case refine_3
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
x y : R
inst✝¹ : Away x S
inst✝ : Away ((algebraMap R S) y) T
a b : R
h : (algebraMap S T) ((algebraMap R S) a) = (algebraMap R T) b
⊢ ∃ n, (y * x) ^ n * a = (y * x) ^ n * b
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case refine_3
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
x y : R
inst✝¹ : Away x S
inst✝ : Away ((algebraMap R S) y) T
a b : R
h : (algebraMap S T) ((algebraMap R S) a) = (algebraMap R T) b
⊢ ∃ n, (y * x) ^ n * a = (y * x) ^ n * b

Tactic:
IsScalarTower.algebraMap_apply R S T

Goal state after:
case refine_3
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
x y : R
inst✝¹ : Away x S
inst✝ : Away ((algebraMap R S) y) T
a b : R
h : (algebraMap S T) ((algebraMap R S) a) = (algebraMap S T) ((algebraMap R S) b)
⊢ ∃ n, (y * x) ^ n * a = (y * x) ^ n * b
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case refine_3
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
x y : R
inst✝¹ : Away x S
inst✝ : Away ((algebraMap R S) y) T
a b : R
h : (algebraMap S T) ((algebraMap R S) a) = (algebraMap S T) ((algebraMap R S) b)
⊢ ∃ n, (y * x) ^ n * a = (y * x) ^ n * b

Tactic:
IsScalarTower.algebraMap_apply R S T

Goal state after:
case refine_3
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
x y : R
inst✝¹ : Away x S
inst✝ : Away ((algebraMap R S) y) T
a b : R
h : (algebraMap S T) ((algebraMap R S) a) = (algebraMap S T) ((algebraMap R S) b)
⊢ ∃ n, (y * x) ^ n * a = (y * x) ^ n * b
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
e : R
he : IsIdempotentElem e
H : ∀ (x y : R), (algebraMap R S) x = (algebraMap R S) y ↔ e * x = e * y
H' : Function.Surjective ⇑(algebraMap R S)
n : ℕ
⊢ e * e = e

Tactic:
he

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
e : R
he : IsIdempotentElem e
H : ∀ (x y : R), (algebraMap R S) x = (algebraMap R S) y ↔ e * x = e * y
H' : Function.Surjective ⇑(algebraMap R S)
n : ℕ
⊢ e = e
Module: Mathlib.RingTheory.Jacobson.Radical

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
ι : Type u_6
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommGroup (M i)
inst✝ : (i : ι) → Module R (M i)
⊢ jacobson R ((i : ι) → M i) ≤ pi Set.univ fun x ↦ jacobson R (M x)

Tactic:
by
  simp_rw [← iInf_comap_proj, jacobson, sInf_eq_iInf', comap_iInf, le_iInf_iff]
  intro i m
  exact iInf_le_of_le ⟨_, (isCoatom_comap_iff <| LinearMap.proj_surjective i).mpr m.2⟩ le_rfl

Goal state after:
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: R : Type u
inst✝ : Ring R
⊢ ⊥.jacobson = Ring.jacobson R

Tactic:
simp_rw [jacobson, Ring.jacobson, Module.jacobson, bot_le, true_and, isMaximal_def]

Goal state after:
Module: Mathlib.RingTheory.Jacobson.Radical

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
ne_bot : N ≠ ⊥
fg : Module.Finite R ↥N
⊢ Ring.jacobson R • N < N

Tactic:
rw [← nontrivial_iff_ne_bot] at ne_bot

Goal state after:
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
ne_bot : Nontrivial ↥N
fg : Module.Finite R ↥N
⊢ Ring.jacobson R • N < N
Module: Mathlib.RingTheory.LocalRing.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
K : Type u_3
inst✝ : Field K
⊢ IsLocalRing K

Tactic:
classical exact IsLocalRing.of_isUnit_or_isUnit_one_sub_self fun a =>
    if h : a = 0 then Or.inr (by rw [h, sub_zero]; exact isUnit_one)
    else Or.inl <| IsUnit.mk0 a h

Goal state after:
Module: Mathlib.RingTheory.LocalRing.RingHom.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : IsLocalRing R
inst✝ : IsLocalRing S
f : R →+* S
hf : Function.Surjective ⇑f
⊢ Ideal.map f (maximalIdeal R) = maximalIdeal S

Tactic:
let := IsLocalHom.of_surjective f hf

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : IsLocalRing R
inst✝ : IsLocalRing S
f : R →+* S
hf : Function.Surjective ⇑f
this : IsLocalHom f := IsLocalHom.of_surjective f hf
⊢ Ideal.map f (maximalIdeal R) = maximalIdeal S
Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial

Goal state before:
pp: case pos.refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
⊢ limit.π F i ≫ eqToHom ⋯ = limit.π F i

Tactic:
eqToHom_refl

Goal state after:
case pos.refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
⊢ limit.π F i ≫ 𝟙 (((Functor.const J).obj (F.1 i)).obj i) = limit.π F i
Module: Mathlib.RingTheory.Localization.Integer

Goal state before:
pp: case mp
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : DecidableEq R
s : Finset S
x : ↥s
⊢ (algebraMap R S) ((fun t ↦ integerMultiple M s id t) x) ∈ commonDenomOfFinset M s • ↑s

Tactic:
rw [map_integerMultiple]

Goal state after:
case mp
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : DecidableEq R
s : Finset S
x : ↥s
⊢ commonDenom M s id • id ↑x ∈ commonDenomOfFinset M s • ↑s
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
M N P : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj P
⊢ (tensorμ (M ⊗ N) P (M ⊗ N) P ≫ (tensorμ M N M N ≫ (μ ⊗ₘ μ) ⊗ₘ μ)) ≫ (α_ M N P).hom =
    ((α_ M N P).hom ⊗ₘ (α_ M N P).hom) ≫ tensorμ M (N ⊗ P) M (N ⊗ P) ≫ (μ ⊗ₘ tensorμ N P N P ≫ (μ ⊗ₘ μ))

Tactic:
simp only [Category.assoc]
  slice_lhs 2 3 => rw [← Category.id_comp μ[P], ← tensorHom_comp_tensorHom]
  slice_lhs 3 4 => rw [associator_naturality]
  slice_rhs 3 4 => rw [← Category.id_comp μ, ← tensorHom_comp_tensorHom]
  simp only [tensorHom_id, id_tensorHom]
  slice_lhs 1 3 => rw [associator_monoidal]
  simp only [Category.assoc]

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

Goal state before:
pp: C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : MonoidalCategory C
M N O X✝ : C
inst✝⁹ : MonObj M
inst✝⁸ : MonObj N
inst✝⁷ : MonObj O
inst✝⁶ : BraidedCategory C
X Y Z W : C
inst✝⁵ : MonObj X
inst✝⁴ : MonObj Y
inst✝³ : MonObj Z
inst✝² : MonObj W
f : X ⟶ Y
g : Z ⟶ W
inst✝¹ : IsMonHom f
inst✝ : IsMonHom g
⊢ η ≫ (f ⊗ₘ g) = η

Tactic:
dsimp [tensorObj.one_def]
    slice_lhs 2 3 => rw [tensorHom_comp_tensorHom, one_hom, one_hom]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case right
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Quiver.IsThin C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
inst✝¹ : Quiver.IsThin D
F : C ⥤ D
inst✝ : PreservesColimitsOfShape (Discrete WalkingPair) F
X Y Z : C
f : Z ⟶ X
g : Z ⟶ Y
hfg : HasPushout f g
⊢ Nonempty (IsColimit (BinaryCofan.mk (F.map (pushout.inl f g)) (F.map (pushout.inr f g))))

Tactic:
refine ⟨(BinaryCofan.mk (pushout.inl f g) (pushout.inr f g)).isColimitMapConeEquiv ?_⟩

Goal state after:
case right
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Quiver.IsThin C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
inst✝¹ : Quiver.IsThin D
F : C ⥤ D
inst✝ : PreservesColimitsOfShape (Discrete WalkingPair) F
X Y Z : C
f : Z ⟶ X
g : Z ⟶ Y
hfg : HasPushout f g
⊢ IsColimit (F.mapCocone (BinaryCofan.mk (pushout.inl f g) (pushout.inr f g)))
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
inst✝ : Subsingleton α
x y : FreeRing α
⊢ x * y = y * x

Tactic:
← (subsingletonEquivFreeCommRing α).symm_apply_apply (y * x),

Goal state after:
α : Type u
inst✝ : Subsingleton α
x y : FreeRing α
⊢ x * y = (subsingletonEquivFreeCommRing α).symm ((subsingletonEquivFreeCommRing α) (y * x))
Module: Mathlib.CategoryTheory.Adjunction.Limits

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type u
inst✝² : Category.{v, u} J
K : J ⥤ D
E : D ⥤ C
inst✝¹ : E.IsEquivalence
inst✝ : HasLimit (K ⋙ E)
⊢ HasLimit K

Tactic:
rw [← hasLimit_iff_of_iso
    (isoWhiskerLeft K E.asEquivalence.unitIso.symm ≪≫ Functor.rightUnitor _)]
  exact hasLimit_comp_equivalence (K ⋙ E) E.inv

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Comonad C
i : T.toFunctor ≅ F
X : C
⊢ T.δ.app X ≫
      T.map (T.δ.app X) ≫ i.hom.app (T.obj (T.obj X)) ≫ F.map (i.hom.app (T.obj X)) ≫ F.map (F.map (i.hom.app X)) =
    T.δ.app X ≫
      T.map (T.δ.app X) ≫ i.hom.app (T.obj (T.obj X)) ≫ F.map (T.map (i.hom.app X)) ≫ F.map (i.hom.app (F.obj X))

Tactic:
simp only [NatTrans.naturality_assoc]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Comonad C
i : T.toFunctor ≅ F
X : C
⊢ T.δ.app X ≫ i.hom.app (T.obj X) ≫ F.map (T.δ.app X) ≫ F.map (i.hom.app (T.obj X)) ≫ F.map (F.map (i.hom.app X)) =
    T.δ.app X ≫ i.hom.app (T.obj X) ≫ F.map (T.δ.app X) ≫ F.map (T.map (i.hom.app X)) ≫ F.map (i.hom.app (F.obj X))
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ ↑⋯.unit⁻¹ (g (b' • a + b • a')) = ↑⋯.unit⁻¹ (g a) + ↑⋯.unit⁻¹ (g a')

Tactic:
rw [map_add, Module.End.algebraMap_isUnit_inv_apply_eq_iff, smul_add, ← map_smul,
        ← map_smul, ← map_smul]

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ g (b' • a) + g (b • a') = ↑⋯.unit⁻¹ (g (↑(b * b') • a)) + ↑⋯.unit⁻¹ (↑(b * b') • g a')
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
l : LocalizedModule S M →ₗ[R] M''
hl : l ∘ₗ mkLinearMap S M = g
m : M
s : ↥S
⊢ ↑⋯.unit⁻¹ (g m) = l (mk m s)

Tactic:
rw [Module.End.algebraMap_isUnit_inv_apply_eq_iff, ← hl, LinearMap.coe_comp,
    Function.comp_apply, LocalizedModule.mkLinearMap_apply, ← l.map_smul, LocalizedModule.smul'_mk]

Goal state after:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
l : LocalizedModule S M →ₗ[R] M''
hl : l ∘ₗ mkLinearMap S M = g
m : M
s : ↥S
⊢ l (mk m 1) = l (mk (↑s • m) s)
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: J : Type u'
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
r : ↑c.pt
h : ∀ (j : J), ∃ b, (ConcreteCategory.hom (c.π.app j)) r * b = 1
⊢ ∃ b, r * b = 1

Tactic:
choose inv h_inv using h

Goal state after:
J : Type u'
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
r : ↑c.pt
inv : (j : J) → ↑(F.obj j)
h_inv : ∀ (j : J), (ConcreteCategory.hom (c.π.app j)) r * inv j = 1
⊢ ∃ b, r * b = 1
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case one
A B : CommRingCat
f g : A ⟶ B
F : WalkingParallelPair ⥤ CommRingCat
x : ↑(limit.cone F).pt
hx : IsUnit ((ConcreteCategory.hom ((limit.cone F).π.app zero)) x)
⊢ ∃ k f g,
    IsLocalHom (Hom.hom (F.map f)) ∧
      (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom ((limit.cone F).π.app one)) x) =
        (ConcreteCategory.hom (F.map g)) ((ConcreteCategory.hom ((limit.cone F).π.app zero)) x)

Tactic:
refine ⟨one, 𝟙 _, left, inferInstance, ?_⟩
    simp only [CategoryTheory.Functor.map_id, hom_id, limit.cone_x, limit.cone_π, RingHom.id_apply]
    exact (limit.w_apply F left x).symm

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

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
X✝ Y✝ : CostructuredArrow (const J) F
f : X✝ ⟶ Y✝
j : J
⊢ f.left ≫ { pt := Y✝.left, π := Y✝.hom }.π.app j = { pt := X✝.left, π := X✝.hom }.π.app j

Tactic:
convert! congr_fun (congr_arg NatTrans.app f.w) j

Goal state after:
case e'_3.e'_7
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
X✝ Y✝ : CostructuredArrow (const J) F
f : X✝ ⟶ Y✝
j : J
e_1✝ :
  ({ pt := X✝.left, π := X✝.hom }.pt ⟶ F.obj j) = (((const J).obj X✝.left).obj j ⟶ ((fromPUnit F).obj Y✝.right).obj j)
e_6✝ : F = (fromPUnit F).obj Y✝.right
⊢ { pt := X✝.left, π := X✝.hom }.π = X✝.hom ≫ (fromPUnit F).map f.right
Module: Mathlib.CategoryTheory.Bicategory.Functor.Oplax

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : B ⥤ᵒᵖᴸ C
G : C ⥤ᵒᵖᴸ D
a✝ b✝ c✝ : B
f✝ f'✝ : a✝ ⟶ b✝
η : f✝ ⟶ f'✝
g : b✝ ⟶ c✝
⊢ G.map₂ (F.map₂ (η ▷ g) ≫ F.mapComp f'✝ g) ≫ G.mapComp (F.map f'✝) (F.map g) =
    (G.map₂ (F.mapComp f✝ g) ≫ G.mapComp (F.map f✝) (F.map g)) ≫ G.map₂ (F.map₂ η) ▷ G.map (F.map g)

Tactic:
mapComp_naturality_left,

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : B ⥤ᵒᵖᴸ C
G : C ⥤ᵒᵖᴸ D
a✝ b✝ c✝ : B
f✝ f'✝ : a✝ ⟶ b✝
η : f✝ ⟶ f'✝
g : b✝ ⟶ c✝
⊢ G.map₂ (F.mapComp f✝ g ≫ F.map₂ η ▷ F.map g) ≫ G.mapComp (F.map f'✝) (F.map g) =
    (G.map₂ (F.mapComp f✝ g) ≫ G.mapComp (F.map f✝) (F.map g)) ≫ G.map₂ (F.map₂ η) ▷ G.map (F.map g)
Module: Mathlib.CategoryTheory.Bicategory.Functor.Oplax

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : B ⥤ᵒᵖᴸ C
G : C ⥤ᵒᵖᴸ D
a✝ b✝ c✝ : B
f✝ f'✝ : a✝ ⟶ b✝
η : f✝ ⟶ f'✝
g : b✝ ⟶ c✝
⊢ G.map₂ (F.mapComp f✝ g) ≫ G.map₂ (F.map₂ η ▷ F.map g) ≫ G.mapComp (F.map f'✝) (F.map g) =
    (G.map₂ (F.mapComp f✝ g) ≫ G.mapComp (F.map f✝) (F.map g)) ≫ G.map₂ (F.map₂ η) ▷ G.map (F.map g)

Tactic:
mapComp_naturality_left,

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : B ⥤ᵒᵖᴸ C
G : C ⥤ᵒᵖᴸ D
a✝ b✝ c✝ : B
f✝ f'✝ : a✝ ⟶ b✝
η : f✝ ⟶ f'✝
g : b✝ ⟶ c✝
⊢ G.map₂ (F.mapComp f✝ g) ≫ G.mapComp (F.map f✝) (F.map g) ≫ G.map₂ (F.map₂ η) ▷ G.map (F.map g) =
    (G.map₂ (F.mapComp f✝ g) ≫ G.mapComp (F.map f✝) (F.map g)) ≫ G.map₂ (F.map₂ η) ▷ G.map (F.map g)
Module: Mathlib.CategoryTheory.Bicategory.Functor.Lax

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F✝ : B ⥤ᴸ C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᴸ C
G : C ⥤ᴸ D
a✝ b✝ c✝ : B
f✝ f'✝ : a✝ ⟶ b✝
η : f✝ ⟶ f'✝
g : b✝ ⟶ c✝
⊢ G.mapComp (F.map f✝) (F.map g) ≫ G.map₂ (F.mapComp f✝ g ≫ F.map₂ (η ▷ g)) =
    G.map₂ (F.map₂ η) ▷ G.map (F.map g) ≫ G.mapComp (F.map f'✝) (F.map g) ≫ G.map₂ (F.mapComp f'✝ g)

Tactic:
mapComp_naturality_left,

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F✝ : B ⥤ᴸ C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᴸ C
G : C ⥤ᴸ D
a✝ b✝ c✝ : B
f✝ f'✝ : a✝ ⟶ b✝
η : f✝ ⟶ f'✝
g : b✝ ⟶ c✝
⊢ G.mapComp (F.map f✝) (F.map g) ≫ G.map₂ (F.map₂ η ▷ F.map g ≫ F.mapComp f'✝ g) =
    G.map₂ (F.map₂ η) ▷ G.map (F.map g) ≫ G.mapComp (F.map f'✝) (F.map g) ≫ G.map₂ (F.mapComp f'✝ g)
Module: Mathlib.CategoryTheory.ObjectProperty.Opposite

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty Cᵒᵖ
⊢ P.isoClosure.unop.op = P.unop.isoClosure.op

Tactic:
P.unop.op_isoClosure,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty Cᵒᵖ
⊢ P.isoClosure.unop.op = P.unop.op.isoClosure
Module: Mathlib.RingTheory.Finiteness.Ideal

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h : I.radical.FG
J : Ideal R
hJ : J.FG
⊢ J ≤ I.radical → ∃ n, J ^ n ≤ I

Tactic:
hJK

Goal state after:
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h : I.radical.FG
J : Ideal R
hJ : J.FG
hJK : J ≤ I.radical
⊢ ∃ n, J ^ n ≤ I
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₁

Goal state after:
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₂ : J), r j₁ j₂
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
h : ∀ (j₁ j₂ : J), ∃ l, List.IsChain Zag (j₁ :: l) ∧ (j₁ :: l).getLast ⋯ = j₂
⊢ ∀ (j₁ j₂ : J), Zigzag j₁ j₂

Tactic:
intro j₁

Goal state after:
J : Type u₁
inst✝ : Category.{v₁, u₁} J
h : ∀ (j₁ j₂ : J), ∃ l, List.IsChain Zag (j₁ :: l) ∧ (j₁ :: l).getLast ⋯ = j₂
j₁ : J
⊢ ∀ (j₂ : J), Zigzag j₁ j₂
Module: Mathlib.CategoryTheory.Limits.Types.Products

Goal state before:
pp: X : Type u
⊢ IsTerminal X ≃ (X ≅ PUnit.{u + 1})

Tactic:
calc
    IsTerminal X ≃ Unique X := isTerminalEquivUnique _
    _ ≃ (X ≃ PUnit) := uniqueEquivEquivUnique _ _
    _ ≃ (X ≅ PUnit) := equivEquivIso

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case h.left
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✝ : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
⊢ Surjective (⇑↑e ∘ ⇑f)

Tactic:
exact Function.Surjective.comp e.surjective hf.1

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case inr
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) := MvPolynomial (Fin n) R
AX : Type (max w₂ 0) := MvPolynomial (Fin n) A
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 := fun x ↦ MvPolynomial.C ↑x - (MvPolynomial.map (algebraMap R A)) (t' x)
s₀ : Set (MvPolynomial (Fin n) A) := ⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
x : A
hx : x ∈ t
⊢ (algebraMap A B) ↑⟨x, hx⟩ - f (t' ⟨x, hx⟩) = 0

Tactic:
ht',

Goal state after:
case inr
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) := MvPolynomial (Fin n) R
AX : Type (max w₂ 0) := MvPolynomial (Fin n) A
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 := fun x ↦ MvPolynomial.C ↑x - (MvPolynomial.map (algebraMap R A)) (t' x)
s₀ : Set (MvPolynomial (Fin n) A) := ⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
x : A
hx : x ∈ t
⊢ (algebraMap A B) ↑⟨x, hx⟩ - (algebraMap A B) ↑⟨x, hx⟩ = 0
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
X Y : Grothendieck F
e₁ : X.base ≅ Y.base
e₂ : (F.map e₁.hom).toFunctor.obj X.fiber ≅ Y.fiber
⊢ (F.map (𝟙 X.base)).toFunctor.obj X.fiber = X.fiber

Tactic:
F.map_id,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
e₁ : X.base ≅ Y.base
e₂ : (F.map e₁.hom).toFunctor.obj X.fiber ≅ Y.fiber
⊢ (𝟙 (F.obj X.base)).toFunctor.obj X.fiber = X.fiber