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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ I.jacobson = I ↔ ⊥.jacobson = ⊥

Tactic:
have hf : Function.Surjective (Ideal.Quotient.mk I) := Submodule.Quotient.mk_surjective I
  constructor
  · intro h
    replace h := congr_arg (Ideal.map (Ideal.Quotient.mk I)) h
    rw [map_jacobson_of_surjective hf (le_of_eq mk_ker)] at h
    simpa using h
  · intro h
    replace h := congr_arg (comap (Ideal.Quotient.mk I)) h
    rw [comap_jacobson_of_surjective hf, ← RingHom.ker_eq_comap_bot (Ideal.Quotient.mk I)] at h
    simpa using h

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

Goal state before:
pp: 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
ι : Type u_4
inst✝ : Finite ι
f : ι → S
⊢ ∃ b, ∀ (i : ι), IsInteger R (↑b • f i)

Tactic:
cases nonempty_fintype ι

Goal state after:
case intro
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
ι : Type u_4
inst✝ : Finite ι
f : ι → S
val✝ : Fintype ι
⊢ ∃ b, ∀ (i : ι), IsInteger R (↑b • f i)
Module: Mathlib.RingTheory.Localization.Integer

Goal state before:
pp: case intro
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
ι : Type u_4
inst✝ : Finite ι
f : ι → S
val✝ : Fintype ι
b : ↥M
hb : ∀ i ∈ Finset.univ, IsInteger R (↑b • f i)
⊢ ∃ b, ∀ (i : ι), IsInteger R (↑b • f i)

Tactic:
exact ⟨b, fun i => hb i (Finset.mem_univ _)⟩

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

Goal state before:
pp: case a.a
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μ N P N P ≫ (μ ⊗ₘ μ)

pp: case a
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
| (α_ M N P).hom ⊗ₘ (α_ M N P).hom

pp: case a.a
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)

Tactic:
← Category.id_comp μ,

Goal state after:
case a.a
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
| 𝟙 (M ⊗ M) ≫ μ ⊗ₘ tensorμ N P N P ≫ (μ ⊗ₘ μ)

case a
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
| (α_ M N P).hom ⊗ₘ (α_ M N P).hom

case a.a
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)
Module: Mathlib.CategoryTheory.Monoidal.Mon

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

Tactic:
← Category.id_comp μ,

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
M : C
inst✝ : MonObj M
⊢ (tensorμ (𝟙_ C) M (𝟙_ C) M ≫ ((λ_ (𝟙_ C)).hom ≫ 𝟙 (𝟙_ C) ⊗ₘ 𝟙 (M ⊗ M) ≫ μ)) ≫ (λ_ M).hom =
    ((λ_ M).hom ⊗ₘ (λ_ M).hom) ≫ 𝟙 (M ⊗ M) ≫ μ
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
v : ι → M
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
t : Finset ι
g₁ g₂ : ι → Rₛ
i : ι
hi : i ∈ t
a : ↥S
fg : ι ⊕ ι → R
hfg :
  (∀ (x : ↥t), (algebraMap R Rₛ) (fg (Sum.inl ↑x)) = ↑a • g₁ ↑x) ∧
    ∀ (x : ↥t), (algebraMap R Rₛ) (fg (Sum.inr ↑x)) = ↑a • g₂ ↑x
eq : ∑ x, (algebraMap R Rₛ) (fg (Sum.inl ↑x)) • (⇑f ∘ v) ↑x = ∑ x, (algebraMap R Rₛ) (fg (Sum.inr ↑x)) • (⇑f ∘ v) ↑x
⊢ g₁ i = g₂ i

Tactic:
algebraMap_smul,

Goal state after:
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
v : ι → M
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
t : Finset ι
g₁ g₂ : ι → Rₛ
i : ι
hi : i ∈ t
a : ↥S
fg : ι ⊕ ι → R
hfg :
  (∀ (x : ↥t), (algebraMap R Rₛ) (fg (Sum.inl ↑x)) = ↑a • g₁ ↑x) ∧
    ∀ (x : ↥t), (algebraMap R Rₛ) (fg (Sum.inr ↑x)) = ↑a • g₂ ↑x
eq : ∑ x, fg (Sum.inl ↑x) • (⇑f ∘ v) ↑x = ∑ x, fg (Sum.inr ↑x) • (⇑f ∘ v) ↑x
⊢ g₁ i = g₂ i
Module: Mathlib.CategoryTheory.Monoidal.Mon

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

Tactic:
← Category.id_comp μ,

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
M : C
inst✝ : MonObj M
⊢ (tensorμ M (𝟙_ C) M (𝟙_ C) ≫ (𝟙 (M ⊗ M) ≫ μ ⊗ₘ (λ_ (𝟙_ C)).hom)) ≫ (ρ_ M).hom =
    ((ρ_ M).hom ⊗ₘ (ρ_ M).hom) ≫ 𝟙 (M ⊗ M) ≫ μ
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
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
inst✝⁶ : MonoidalCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : MonoidalCategory E
F F' : C ⥤ D
G : D ⥤ E
inst✝³ : F.Monoidal
hF : F.FullyFaithful
X Y : C
inst✝² : AddMonObj X
inst✝¹ : AddMonObj Y
f : F.obj X ⟶ F.obj Y
inst✝ : IsAddMonHom f
⊢ F.map (AddMonObj.add ≫ hF.preimage f) = F.map ((hF.preimage f ⊗ₘ hF.preimage f) ≫ AddMonObj.add)

Tactic:
by
    simp [← obj.σ_def_assoc, ← obj.σ_def, ← μ_natural_assoc, ← cancel_epi (LaxMonoidal.μ F ..)]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
c : BinaryFan X Y
h : IsLimit c
t : IsTerminal Z
⊢ ∀ (j : Discrete WalkingPair),
    c.π.app j =
      (Iso.refl c.pt).hom ≫
        (BinaryFan.mk (c.π.1 { as := WalkingPair.left }) (c.π.1 { as := WalkingPair.right })).π.app j

Tactic:
rintro ⟨⟨⟩⟩ <;> simp

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

Goal state before:
pp: case commf
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P' ≅ P
e₂ : X' ≅ X
e₃ : Y' ≅ Y
e₄ : Z' ≅ Z
commfst : e₁.hom ≫ fst = fst' ≫ e₂.hom
commsnd : e₁.hom ≫ snd = snd' ≫ e₃.hom
commf : e₂.hom ≫ f = f' ≫ e₄.hom
commg : e₃.hom ≫ g = g' ≫ e₄.hom
⊢ f ≫ e₄.symm.hom = e₂.symm.hom ≫ f'

pp: case commg
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P' ≅ P
e₂ : X' ≅ X
e₃ : Y' ≅ Y
e₄ : Z' ≅ Z
commfst : e₁.hom ≫ fst = fst' ≫ e₂.hom
commsnd : e₁.hom ≫ snd = snd' ≫ e₃.hom
commf : e₂.hom ≫ f = f' ≫ e₄.hom
commg : e₃.hom ≫ g = g' ≫ e₄.hom
⊢ g ≫ e₄.symm.hom = e₃.symm.hom ≫ g'

Tactic:
· simp only [Iso.symm_hom, Iso.comp_inv_eq, Category.assoc, ← commf, Iso.inv_hom_id_assoc]

Goal state after:
case commg
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P' ≅ P
e₂ : X' ≅ X
e₃ : Y' ≅ Y
e₄ : Z' ≅ Z
commfst : e₁.hom ≫ fst = fst' ≫ e₂.hom
commsnd : e₁.hom ≫ snd = snd' ≫ e₃.hom
commf : e₂.hom ≫ f = f' ≫ e₄.hom
commg : e₃.hom ≫ g = g' ≫ e₄.hom
⊢ g ≫ e₄.symm.hom = e₃.symm.hom ≫ g'
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: case h₀
C : Type u
inst✝ : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit t₁
s : PullbackCone (g₁ ≫ g₂) i₃
l₂ : s.pt ⟶ t₂.pt
hl₂ : l₂ ≫ t₂.fst = s.fst ≫ g₁
hl₂' : l₂ ≫ t₂.snd = s.snd
l₁ : s.pt ⟶ t₁.pt
hl₁ : l₁ ≫ t₁.fst = s.fst
hl₁' : l₁ ≫ t₁.snd = l₂
m : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hm₁ : m ≫ t₁.fst = s.fst
hm₂ : m ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd
⊢ (m ≫ t₁.snd) ≫ t₂.fst = (l₁ ≫ t₁.snd) ≫ t₂.fst

Tactic:
rw [Category.assoc, ← hi₂, ← t₁.condition, reassoc_of% hm₁, hl₁', hi₂, hl₂]

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
⊢ (algebraMap R A) ↑s • (mk' A r s • x✝¹) ⊗ₜ[R] x✝ = (algebraMap R A) ↑s • x✝¹ ⊗ₜ[R] (mk' A r s • x✝)

Tactic:
algebraMap_smul,

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
⊢ ↑s • (mk' A r s • x✝¹) ⊗ₜ[R] x✝ = ↑s • x✝¹ ⊗ₜ[R] (mk' A r s • x✝)
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
⊢ ((algebraMap R A) r • x✝¹) ⊗ₜ[R] x✝ = x✝¹ ⊗ₜ[R] ((algebraMap R A) r • x✝)

Tactic:
algebraMap_smul,

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
⊢ (r • x✝¹) ⊗ₜ[R] x✝ = x✝¹ ⊗ₜ[R] (r • x✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y : C
c : BinaryCofan X Y
h : IsColimit c
t : IsInitial Z
⊢ ∀ (j : Discrete WalkingPair),
    c.ι.app j ≫ (Iso.refl c.pt).hom =
      (BinaryCofan.mk (c.ι.1 { as := WalkingPair.left }) (c.ι.1 { as := WalkingPair.right })).ι.app j

Tactic:
rintro ⟨⟨⟩⟩ <;> simp

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

Goal state before:
pp: 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
⊢ ∃ P inl inr, IsPushout f g inl inr ∧ IsPushout (F.map f) (F.map g) (F.map inl) (F.map inr)

Tactic:
use pushout f g, pushout.inl f g, pushout.inr f g, .of_hasPushout f g

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
⊢ IsPushout (F.map f) (F.map g) (F.map (pushout.inl f g)) (F.map (pushout.inr f g))
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: A B : CommRingCat
s : BinaryCofan A B
⊢ ∀ (m : (A.coproductCocone B).pt ⟶ s.pt),
    (∀ (j : Discrete WalkingPair), (A.coproductCocone B).ι.app j ≫ m = s.ι.app j) →
      m = ofHom (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom ⋯).toRingHom

Tactic:
rintro ⟨m : A ⊗[ℤ] B →+* s.pt⟩ hm

Goal state after:
A B : CommRingCat
s : BinaryCofan A B
m : ↑A ⊗[ℤ] ↑B →+* ↑s.pt
hm : ∀ (j : Discrete WalkingPair), (A.coproductCocone B).ι.app j ≫ { hom' := m } = s.ι.app j
⊢ { hom' := m } = ofHom (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom ⋯).toRingHom
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
η : a✝ ⟶ b✝
⊢ ∀ {g g' : b✝ ⟶ c✝} (η_1 : g ⟶ g'),
    (F.comp G.toPrelaxFunctor).map₂ (η ◁ η_1) ≫
        (G.mapFunctor (F.obj a✝) (F.obj c✝)).map (F.mapComp η g') ≫ G.mapComp (F.map η) (F.map g') =
      ((G.mapFunctor (F.obj a✝) (F.obj c✝)).map (F.mapComp η g) ≫ G.mapComp (F.map η) (F.map g)) ≫
        (F.comp G.toPrelaxFunctor).map η ◁ (F.comp G.toPrelaxFunctor).map₂ η_1

Tactic:
by
    dsimp
    intros
    rw [← G.map₂_comp_assoc, mapComp_naturality_right, G.map₂_comp_assoc,
      mapComp_naturality_right, assoc]

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

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
ι : Type u_1
X : ι → C
Z : Cᵒᵖ
i : ι
hi : op (X i) = Z
⊢ X i = unop Z

Tactic:
rw [← hi]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
I : Ideal R
inst✝ : I.IsTwoSided
n : ℕ
hI : I.FG
⊢ (I ^ Nat.zero).FG

Tactic:
rw [I.pow_zero, one_eq_top]; exact fg_top R

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case h.right
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
hco : ((↑e).comp f).toRingHom = (↑e.toRingEquiv).comp f.toRingHom
⊢ Ideal.comap ((↑e.toRingEquiv).comp f.toRingHom) ⊥ = RingHom.ker f.toRingHom

Tactic:
← Ideal.comap_comap,

Goal state after:
case h.right
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
hco : ((↑e).comp f).toRingHom = (↑e.toRingEquiv).comp f.toRingHom
⊢ Ideal.comap f.toRingHom (Ideal.comap ↑e.toRingEquiv ⊥) = RingHom.ker f.toRingHom
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: R : Type w₁
inst✝¹ : CommRing R
ι : Type u_1
inst✝ : Finite ι
⊢ ∃ n f, Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG

Tactic:
cases nonempty_fintype ι

Goal state after:
case intro
R : Type w₁
inst✝¹ : CommRing R
ι : Type u_1
inst✝ : Finite ι
val✝ : Fintype ι
⊢ ∃ n f, Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: 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
f : A →ₐ[R] B
hf : Surjective ⇑f
inst✝¹ : FinitePresentation R A
inst✝ : FinitePresentation R B
n : ℕ
g : MvPolynomial (Fin n) R →ₐ[R] A
hg : Surjective ⇑g
right✝ : (RingHom.ker g.toRingHom).FG
⊢ Ideal.comap ↑f ⊥ = Ideal.map (↑g) (Ideal.comap ((↑f).comp ↑g) ⊥)

Tactic:
← Ideal.comap_comap,

Goal state after:
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
f : A →ₐ[R] B
hf : Surjective ⇑f
inst✝¹ : FinitePresentation R A
inst✝ : FinitePresentation R B
n : ℕ
g : MvPolynomial (Fin n) R →ₐ[R] A
hg : Surjective ⇑g
right✝ : (RingHom.ker g.toRingHom).FG
⊢ Ideal.comap ↑f ⊥ = Ideal.map (↑g) (Ideal.comap (↑g) (Ideal.comap ↑f ⊥))
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ fst (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ diagonal i ≫ fst i i =
    (pullbackDiagonalMapIdIso f g i).hom ≫ fst f g ≫ f

Tactic:
pullback.condition_assoc

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯ ≫ fst i i =
    (pullbackDiagonalMapIdIso f g i).hom ≫ fst f g ≫ f
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: case refine_2
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
⊢ ∀ {X Y Z : CommRingCat} (e : Y ≅ Z) (f : X ⟶ Y),
    toMorphismProperty (fun {R S} [CommRing R] [CommRing S] ↦ P) f →
      toMorphismProperty (fun {R S} [CommRing R] [CommRing S] ↦ P) (f ≫ e.hom)

Tactic:
intro X Y Z e f hf
    exact h.left f.hom e.commRingCatIsoToRingEquiv hf

Goal state after:
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], Q (algebraMap R S) → P (algebraMap S (S ⊗[R] T)) → P (algebraMap R T)
⊢ CodescendsAlong (fun {R S} [CommRing R] [CommRing S] ↦ P) fun {R S} [CommRing R] [CommRing S] ↦ Q

Tactic:
by
  introv R h hQ H
  let e := h.symm.equiv
  have : (e.symm : _ →+* _).comp (algebraMap R' S') = algebraMap R' (R' ⊗[R] S) := by
    ext r
    simp [e]
  apply h₂ hQ
  rw [← this]
  exact h₁.1 _ _ H

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ fst (snd f' g') i₂ ≫ snd f' g' ≫ g' =
    snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (snd f' g') i₂ ≫ i₂ ≫ g'

Tactic:
pullback.condition_assoc

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (snd f' g') i₂ ≫ i₂ ≫ g' =
    snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (snd f' g') i₂ ≫ i₂ ≫ g'
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : CartesianMonoidalCategory C
F : Cᵒᵖ ⥤ MonCat
⊢ (F ⋙ forget MonCat).IsRepresentable → yonedaMon.essImage F

Tactic:
· rintro ⟨X, ⟨e⟩⟩
    let := MonObj.ofRepresentableBy X F e
    exact ⟨Mon.mk X, ⟨yonedaMonObjIsoOfRepresentableBy X F e⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: case η
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : CartesianMonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : CartesianMonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : CartesianMonoidalCategory E
F : C ⥤ D
G : D ⥤ E
X Y Z : C
inst✝¹ : F.OplaxMonoidal
inst✝ : PreservesFiniteProducts F
a b : F.OplaxMonoidal
⊢ η F = η F

Tactic:
exact toUnit_unique _ _

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
ι : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a : A
repr : Coalgebra.Repr R a ι
⊢ ∑ i ∈ repr.index, repr.left i * (antipode R) (repr.right i) = counit a • 1

Tactic:
rw [sum_mul_antipode_eq_algebraMap_counit, Algebra.smul_def, mul_one]

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
⊢ counit ∘ₗ antipode R = counit

Tactic:
by
  ext; exact counit_antipode _

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

Goal state before:
pp: R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
f : ι →₀ R
i : ι
⊢ ((Finsupp.linearCombination R ⇑b.dualBasis) f) (b i) = f i

Tactic:
cases nonempty_fintype ι

Goal state after:
case intro
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
f : ι →₀ R
i : ι
val✝ : Fintype ι
⊢ ((Finsupp.linearCombination R ⇑b.dualBasis) f) (b i) = f i
Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this✝¹ : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Module.Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun i ↦ bK i.1 i.2)
this✝ : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)
ιL : Type u
bL : Module.Basis ιL (↥L)ᵐᵒᵖ K
hLK : #ιL < ℵ₀
this : Fintype ιL
⊢ #K ≤ #↥L

Tactic:
rw [bL.repr.toEquiv.cardinal_eq, mk_finsupp_of_fintype,
        ← MulOpposite.opEquiv.cardinal_eq] at card_K ⊢

Goal state after:
K : Type u
inst✝ : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
this✝¹ : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Module.Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun i ↦ bK i.1 i.2)
this✝ : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)
ιL : Type u
bL : Module.Basis ιL (↥L)ᵐᵒᵖ K
hLK : #ιL < ℵ₀
this : Fintype ιL
card_K : ℵ₀ < #↥L ^ Fintype.card ιL
⊢ #↥L ^ Fintype.card ιL ≤ #↥L
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type uR
M : Type uM
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_1
inst✝ : Finite ι
b : Basis ι R M
⊢ (Dual.eval R M).range = ⊤

Tactic:
cases nonempty_fintype ι

Goal state after:
case intro
R : Type uR
M : Type uM
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_1
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
⊢ (Dual.eval R M).range = ⊤
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
l : ι →₀ R
i : ι
⊢ (h.coeffs (lc e l)) i = l i

Tactic:
rw [h.coeffs_apply, h.dual_lc]

Goal state after: