mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: case tmul
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
Y Y' : ModuleCat S
g : Y ⟶ Y'
m1 : Module R S := Module.compHom S f
m2✝ : Module R ↑Y := Module.compHom (↑Y) f
m2 : Module R ↑Y' := Module.compHom (↑Y') f
s' : ↑((restrictScalars f).obj (of S S))
y : ↑((restrictScalars f).obj Y)
⊢ (Hom.hom (Counit.map f)) (s' ⊗ₜ[R] (ConcreteCategory.hom g) y) = (Hom.hom g) ((Hom.hom (Counit.map f)) (s' ⊗ₜ[R] y))

Tactic:
Counit.map_hom_apply

Goal state after:
case tmul
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
Y Y' : ModuleCat S
g : Y ⟶ Y'
m1 : Module R S := Module.compHom S f
m2✝ : Module R ↑Y := Module.compHom (↑Y) f
m2 : Module R ↑Y' := Module.compHom (↑Y') f
s' : ↑((restrictScalars f).obj (of S S))
y : ↑((restrictScalars f).obj Y)
⊢ (lift { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
      (s' ⊗ₜ[R] (ConcreteCategory.hom g) y) =
    (Hom.hom g) ((Hom.hom (Counit.map f)) (s' ⊗ₜ[R] y))
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝⁵ : CommRing R✝
inst✝⁴ : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : Ring S
f : R →+* S
J : Type u_3
inst✝¹ : Category.{v_1, u_3} J
F : J ⥤ ModuleCat S
inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat S) AddCommGrpCat)
this : HasColimit ((F ⋙ restrictScalars f) ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
⊢ IsColimit
    ((forget₂ (ModuleCat R) AddCommGrpCat).mapCocone ((restrictScalars f).mapCocone (HasColimit.colimitCocone F)))

Tactic:
apply isColimitOfPreserves (forget₂ (ModuleCat.{v} S) AddCommGrpCat.{v})

Goal state after:
R✝ : Type u₁
S✝ : Type u₂
inst✝⁵ : CommRing R✝
inst✝⁴ : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : Ring S
f : R →+* S
J : Type u_3
inst✝¹ : Category.{v_1, u_3} J
F : J ⥤ ModuleCat S
inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat S) AddCommGrpCat)
this : HasColimit ((F ⋙ restrictScalars f) ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
⊢ IsColimit (HasColimit.colimitCocone F)
Module: Mathlib.CategoryTheory.Adjunction.Unique

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F F' F'' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
adj3 : F'' ⊣ G
x : C
⊢ (adj1.leftAdjointUniq adj2).hom.app x ≫ (adj2.leftAdjointUniq adj3).hom.app x = (adj1.leftAdjointUniq adj3).hom.app x

Tactic:
rw [← leftAdjointUniq_trans adj1 adj2 adj3]
  rfl

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

Goal state before:
pp: R : Type u_1
M : Type u_3
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₁ : Type u_14
N₂ : Type u_15
N₃ : Type u_16
inst✝¹⁴ : CommSemiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : AddCommMonoid N₁
inst✝⁷ : AddCommMonoid N₂
inst✝⁶ : AddCommMonoid N₃
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N₃
f₁ : M₁ →ₗ[R] N₁
f₂ : M₂ →ₗ[R] N₂
f₃ : M₃ →ₗ[R] N₃
f₁₂ : M →ₗ[R] M₁ ⊗[R] M₂
f : M →ₗ[R] M ⊗[R] M₃
⊢ α ∘ₗ (f₁ ⊗ₘ f₂ ∘ₗ f₁₂) ⊗ₘ f₃ ∘ₗ f = f₁ ⊗ₘ (f₂ ⊗ₘ f₃) ∘ₗ α ∘ₗ f₁₂ ⊗ₘ LinearMap.id ∘ₗ f

Tactic:
by
  simp only [← LinearMap.comp_assoc, assoc_comp_map_map_comp]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
M' : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Coalgebra R M
f : M →ₗ[R] M'
⊢ f ⊗ₘ ε ∘ₗ δ = f ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹

Tactic:
rw [← LinearMap.rTensor_comp_lTensor, LinearMap.comp_assoc, Coalgebra.lTensor_counit_comp_comul]
  rfl

Goal state after:
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
P : Type u_3
inst✝⁴ : CommSemiring P
Q : Type u_4
inst✝³ : CommSemiring Q
inst✝² : Algebra P Q
f : R →+* P
r : R
inst✝¹ : Away r S
inst✝ : Away (f r) Q
⊢ (∀ (a : P) (n : ℕ), ∃ b m k, f (r ^ (k + n) * b) = f r ^ (k + m) * a) ↔ ∀ (a : P), ∃ b m, f b = f r ^ m * a

Tactic:
refine ⟨fun H x ↦ ⟨_, _, (H x 0).choose_spec.choose_spec.choose_spec⟩, fun H a n ↦ ?_⟩
    obtain ⟨b, m, e⟩ := H a
    exact ⟨b, n + m, 0, by simp [e, pow_add]; ring_nf⟩

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 : N.FG
⊢ Ring.jacobson R • N < N

Tactic:
rw [← Module.Finite.iff_fg] at fg
  rw [← nontrivial_iff_ne_bot] at ne_bot
  convert! map_strictMono_of_injective N.injective_subtype (jacobson_smul_lt_top ⊤)
  on_goal 1 => rw [map_smul'']
  all_goals rw [Submodule.map_top, range_subtype]

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
hPunique : ∀ (y : Ideal R), (fun P ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = P
hPnonzero : P ≠ ⊥
hPnot_top : P ≠ ⊤
mem_or_mem'✝ : ∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P
M : Ideal R
hM : (fun I ↦ I.IsMaximal) M
⊢ M ≠ ⊥

Tactic:
· rintro rfl
        exact hPnot_top (hM.1.2 P (bot_lt_iff_ne_bot.2 hPnonzero))

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : IsLocalRing R
inst✝² : CommSemiring S
inst✝¹ : IsLocalRing S
f : R →+* S
inst✝ : IsLocalHom f
⊢ Ideal.map f (maximalIdeal R) ≤ maximalIdeal S

Tactic:
Ideal.map_le_iff_le_comap,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : IsLocalRing R
inst✝² : CommSemiring S
inst✝¹ : IsLocalRing S
f : R →+* S
inst✝ : IsLocalHom f
⊢ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasStrictInitialObjects C
I : C
hI : IsInitial I
A : C
f g : A ⟶ I
⊢ f = g

Tactic:
have := hI.isIso_to f
  have := hI.isIso_to g
  exact eq_of_inv_eq_inv (hI.hom_ext (inv f) (inv g))

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
T : Type u_5
B : Type u_6
inst✝⁷ : CommSemiring T
inst✝⁶ : CommSemiring B
inst✝⁵ : Algebra R T
inst✝⁴ : Algebra T B
inst✝³ : Algebra R B
inst✝² : Algebra A B
inst✝¹ : IsScalarTower R T B
inst✝ : IsScalarTower R A B
⊢ IsLocalization (algebraMapSubmonoid T S) B ↔ IsBaseChange A (IsScalarTower.toAlgHom R T B).toLinearMap

Tactic:
← isLocalizedModule_iff_isLocalization

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
T : Type u_5
B : Type u_6
inst✝⁷ : CommSemiring T
inst✝⁶ : CommSemiring B
inst✝⁵ : Algebra R T
inst✝⁴ : Algebra T B
inst✝³ : Algebra R B
inst✝² : Algebra A B
inst✝¹ : IsScalarTower R T B
inst✝ : IsScalarTower R A B
⊢ IsLocalizedModule S (IsScalarTower.toAlgHom R T B).toLinearMap ↔
    IsBaseChange A (IsScalarTower.toAlgHom R T B).toLinearMap
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ Y₁ : C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
i₁ : X₁ ⟶ Y₁
t₁ : PushoutCocone i₁ f₁
i₂ : X₂ ⟶ t₁.pt
t₂ : PushoutCocone «i₂» f₂
hi₂ : «i₂» = t₁.inr
H : IsColimit t₁
H' : IsColimit t₂
s : PushoutCocone i₁ (f₁ ≫ f₂)
l₁ : t₁.pt ⟶ s.pt
hl₁ : t₁.inl ≫ l₁ = s.inl
hl₁' : t₁.inr ≫ l₁ = f₂ ≫ s.inr
l₂ : t₂.pt ⟶ s.pt
hl₂ : t₂.inl ≫ l₂ = l₁
hl₂' : t₂.inr ≫ l₂ = s.inr
m : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hm₁ : (t₁.pasteHoriz t₂ hi₂).inl ≫ m = s.inl
hm₂ : (t₁.pasteHoriz t₂ hi₂).inr ≫ m = s.inr
⊢ t₂.inr ≫ m = t₂.inr ≫ l₂

Tactic:
simpa [hl₂'] using hm₂

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_3
inst✝¹⁹ : AddCommMonoid M✝
inst✝¹⁸ : Module R✝ M✝
M' : Type u_4
inst✝¹⁷ : AddCommMonoid M'
inst✝¹⁶ : Module R✝ M'
inst✝¹⁵ : Module A✝ M'
inst✝¹⁴ : IsScalarTower R✝ A✝ M'
f : M✝ →ₗ[R✝] M'
T : Type u_5
B : Type u_6
inst✝¹³ : CommSemiring T
inst✝¹² : CommSemiring B
inst✝¹¹ : Algebra R✝ T
inst✝¹⁰ : Algebra T B
inst✝⁹ : Algebra R✝ B
inst✝⁸ : Algebra A✝ B
inst✝⁷ : IsScalarTower R✝ T B
inst✝⁶ : IsScalarTower R✝ A✝ B
R : Type u_7
S : Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
r : R
A : Type u_9
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
M : Submonoid R
inst✝ : IsLocalization M A
⊢ IsLocalization (Algebra.algebraMapSubmonoid S M) (S ⊗[R] A)

Tactic:
by
  let _ : Algebra A (S ⊗[R] A) := Algebra.TensorProduct.rightAlgebra
  rw [Algebra.isLocalization_iff_isPushout _ A]
  infer_instance

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
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
⊢ IsColimit (Cofork.ofπ g ⋯)

Tactic:
fapply Cofork.IsColimit.mk
  · exact fun s => H.isColimit.desc (PushoutCocone.mk s.π s.π s.condition)
  · exact fun s => H.isColimit.fac _ WalkingSpan.left
  · intro s m e
    apply PushoutCocone.IsColimit.hom_ext H.isColimit <;> refine e.trans ?_ <;> symm <;>
      exact H.isColimit.fac _ _

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
R : Type v
inst✝ : CommRing R
f✝ f : α → R
x y : Multiplicative (Multiset α)
⊢ (Multiset.map f (Multiplicative.toAdd (x * y))).prod = (Multiset.map f x + Multiset.map f y).prod

Tactic:
rw [← Multiset.map_add]
            rfl

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
P X Y Z : C
inl : X ⟶ P
inr : Y ⟶ P
f : Z ⟶ X
g : Z ⟶ Y
h : IsPushout f g inl inr
⊢ PreservesColimit (span f g) F ↔ IsPushout (F.map f) (F.map g) (F.map inl) (F.map inr)

Tactic:
by
  refine ⟨fun _ ↦ h.map _, fun hF ↦ ?_⟩
  apply preservesColimit_of_preserves_colimit_cocone h.isColimit
  exact (PushoutCocone.isColimitMapCoconeEquiv _ _).symm hF.isColimit

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: case mul
α : Type u
x✝ y✝ : FreeCommRing α
hx : ∃ a, ↑a = x✝
hy : ∃ a, ↑a = y✝
⊢ ∃ a, ↑a = x✝ * y✝

Tactic:
| mul _ _ hx hy =>

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Submonoid R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : R
s : ↥S
⊢ (algebraMap (Localization S) (LocalizedModule S A)) (IsLocalization.mk' (Localization S) a s) =
    mk ((algebraMap R A) a) s

Tactic:
exact algebraMap_mk' ..

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Units

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup Gˣ
x : G
⊢ (∃ x_1, toUnits x_1 ∈ H ∧ x_1 = x) ↔ toUnits x ∈ H

Tactic:
exists_eq_right

Goal state after:
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_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : Module R M
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
N : Type u_6
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
g : M' →ₗ[R] N
H : ∀ {x y : M}, g (f x) = g (f y) → f x = f y
a b : M'
hab : g a = g b
x : M
m : ↥S
hxm : m • a = f x
y : M
n : ↥S
hym : n • b = f y
h : ↑n • f x = ↑m • f y
⊢ n • m • a = m • n • b

Tactic:
hxm,

Goal state after:
R : Type u_1
inst✝⁷ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : Module R M
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
N : Type u_6
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
g : M' →ₗ[R] N
H : ∀ {x y : M}, g (f x) = g (f y) → f x = f y
a b : M'
hab : g a = g b
x : M
m : ↥S
hxm : m • a = f x
y : M
n : ↥S
hym : n • b = f y
h : ↑n • f x = ↑m • f y
⊢ n • f x = m • n • b
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:
dsimp
    intros
    rw [← G.map₂_comp_assoc, mapComp_naturality_right, G.map₂_comp_assoc,
      mapComp_naturality_right, assoc]

Goal state after:
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
a b : B
f : a ⟶ b
⊢ (λ_ (F.map f)).hom = F.mapId a ▷ F.map f ≫ F.mapComp (𝟙 a) f ≫ F.map₂ (λ_ f).hom

Tactic:
rw [← PrelaxFunctor.map₂Iso_hom, ← assoc, ← Iso.comp_inv_eq, ← Iso.eq_inv_comp]

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤ᴸ C
a b : B
f : a ⟶ b
⊢ (F.map₂Iso (λ_ f)).inv = (λ_ (F.map f)).inv ≫ F.mapId a ▷ F.map f ≫ F.mapComp (𝟙 a) f
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
a b : B
f : a ⟶ b
⊢ (ρ_ (F.map f)).hom = F.map f ◁ F.mapId b ≫ F.mapComp f (𝟙 b) ≫ F.map₂ (ρ_ f).hom

Tactic:
rw [← PrelaxFunctor.map₂Iso_hom, ← assoc, ← Iso.comp_inv_eq, ← Iso.eq_inv_comp]

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤ᴸ C
a b : B
f : a ⟶ b
⊢ (F.map₂Iso (ρ_ f)).inv = (ρ_ (F.map f)).inv ≫ F.map f ◁ F.mapId b ≫ F.mapComp f (𝟙 b)
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 : a✝ ⟶ b✝
x✝¹ x✝ : b✝ ⟶ c✝
η : x✝¹ ⟶ x✝
⊢ G.mapComp (F.map f) (F.map x✝¹) ≫ G.map₂ (F.map f ◁ F.map₂ η) ≫ G.map₂ (F.mapComp f x✝) =
    G.map (F.map f) ◁ G.map₂ (F.map₂ η) ≫ G.mapComp (F.map f) (F.map x✝) ≫ G.map₂ (F.mapComp f x✝)

Tactic:
mapComp_naturality_right_assoc

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 : a✝ ⟶ b✝
x✝¹ x✝ : b✝ ⟶ c✝
η : x✝¹ ⟶ x✝
⊢ G.map (F.map f) ◁ G.map₂ (F.map₂ η) ≫ G.mapComp (F.map f) (F.map x✝) ≫ G.map₂ (F.mapComp f x✝) =
    G.map (F.map f) ◁ G.map₂ (F.map₂ η) ≫ G.mapComp (F.map f) (F.map x✝) ≫ G.map₂ (F.mapComp f x✝)
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
P : ObjectProperty Cᵒᵖ
inst✝ : ObjectProperty.Small.{w, v, u} P
⊢ ObjectProperty.Small.{w, v, u} P.unop

Tactic:
by
  simpa only [← small_congr P.unop.subtypeOpEquiv]

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

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
hQ : P ≤ Q.isoClosure
P' : ObjectProperty C := Q ⊓ P.isoClosure
φ : Subtype P' → Subtype P
hφ : ∀ (X' : Subtype P'), Nonempty (↑X' ≅ ↑(φ X'))
⊢ ObjectProperty.Small.{w, v, u} fun X ↦ X ∈ Set.range (Subtype.val ∘ φ)

Tactic:
exact small_of_surjective (f := fun X ↦ ⟨(φ X).1, by tauto⟩)
      (by rintro ⟨_, Z, rfl⟩; exact ⟨Z, rfl⟩)

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

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
X : C
inst✝² : IsConnected J
F : J ⥤ C
inst✝¹ : HasLimit F
c : Cone F
inst✝ : IsIso (limMap c.π)
⊢ IsLimit c

Tactic:
by
  refine IsLimit.ofIsoLimit (limit.isLimit _) (Cone.ext ((asIso (limMap c.π)).symm ≪≫
    (limit.isLimit _).conePointUniqueUpToIso (isLimitConstCone J c.pt)) ?_)
  intro j
  simp only [limit.cone_x, limit.cone_π, Iso.trans_hom, Iso.symm_hom,
    asIso_inv, assoc, IsIso.eq_inv_comp, limMap_π]
  congr 1
  simp [← Iso.inv_comp_eq_id]

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
f : X ⟶ Y
inst✝¹ : HasPullback f f
inst✝ : Mono f
⊢ IsIso (diagonal f)

Tactic:
rw [(IsIso.inv_eq_of_inv_hom_id (diagonal_fst f)).symm]
  infer_instance

Goal state after:
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange P
hP' : RespectsIso P
R S T : CommRingCat
f : R ⟶ S
g : R ⟶ T
H : P (CommRingCat.Hom.hom g)
this✝ : Algebra ↑R ↑S := ⋯
this : Algebra ↑R ↑T := ⋯
⊢ P (algebraMap ↑R ↑T)

Tactic:
exact H

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝² : Category.{v', u'} J
J' : Type u''
inst✝¹ : Category.{v'', u''} J'
e : J ≌ J'
inst✝ : P.IsClosedUnderLimitsOfShape J
⊢ P.IsClosedUnderLimitsOfShape J'

Tactic:
by
  rwa [← P.isClosedUnderLimitsOfShape_iff_of_equivalence e]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts

Goal state before:
pp: case refine_2
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone (Discrete.functor f)
j : Fin (n + 1)
i : Fin n
⊢ c₁.ι.app { as := i } ≫
      c₂.inr ≫
        ↑(BinaryCofan.IsColimit.desc' t₂ (s.ι.app { as := 0 })
            (t₁.desc { pt := s.pt, ι := Discrete.natTrans fun i ↦ s.ι.app { as := i.as.succ } })) =
    s.ι.app { as := i.succ }

Tactic:
(BinaryCofan.IsColimit.desc' t₂ _ _).2.2,

Goal state after:
case refine_2
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone (Discrete.functor f)
j : Fin (n + 1)
i : Fin n
⊢ c₁.ι.app { as := i } ≫ t₁.desc { pt := s.pt, ι := Discrete.natTrans fun i ↦ s.ι.app { as := i.as.succ } } =
    s.ι.app { as := i.succ }
Module: Mathlib.CategoryTheory.ObjectProperty.Retract

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

Tactic:
by
  refine le_antisymm ?_ (monotone_retractClosure P.le_isoClosure)
  rintro Y ⟨X, ⟨X', hX', ⟨e⟩⟩, ⟨h⟩⟩
  exact ⟨_, hX', ⟨h.trans (Retract.ofIso e)⟩⟩

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 : C
f : X ⟶ Y
inst✝ : HasPushout f f
H : IsIso (codiagonal f)
Z✝ : C
x✝¹ x✝ : Y ⟶ Z✝
e : f ≫ x✝¹ = f ≫ x✝
⊢ x✝¹ = x✝

Tactic:
← inl_desc _ _ e,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst✝ : HasPushout f f
H : IsIso (codiagonal f)
Z✝ : C
x✝¹ x✝ : Y ⟶ Z✝
e : f ≫ x✝¹ = f ≫ x✝
⊢ inl f f ≫ desc x✝¹ x✝ e = x✝
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : GrpObj A
⊢ (ι ⊗ₘ ι) ≫ μ = (β_ A A).hom ≫ μ ≫ ι

Tactic:
rw [mul_inv A, SymmetricCategory.symmetry_assoc]

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

Goal state before:
pp: case zero
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
hba : b ≠ a
m : ℕ
h :
  (fun n ↦
        have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
        this)
      0 =
    (fun n ↦
        have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
        this)
      m
⊢ 0 = m

Tactic:
rcases m with - | m

Goal state after:
case zero.zero
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
hba : b ≠ a
h :
  (fun n ↦
        have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
        this)
      0 =
    (fun n ↦
        have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
        this)
      0
⊢ 0 = 0

case zero.succ
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
hba : b ≠ a
m : ℕ
h :
  (fun n ↦
        have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
        this)
      0 =
    (fun n ↦
        have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
        this)
      (m + 1)
⊢ 0 = m + 1
Module: Mathlib.Data.W.Basic

Goal state before:
pp: case succ
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
hba : b ≠ a
n : ℕ
ih :
  ∀ ⦃m : ℕ⦄,
    (fun n ↦
            have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
            this)
          n =
        (fun n ↦
            have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
            this)
          m →
      n = m
m : ℕ
h :
  (fun n ↦
        have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
        this)
      (n + 1) =
    (fun n ↦
        have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
        this)
      m
⊢ n + 1 = m

Tactic:
rcases m with - | m

Goal state after:
case succ.zero
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
hba : b ≠ a
n : ℕ
ih :
  ∀ ⦃m : ℕ⦄,
    (fun n ↦
            have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
            this)
          n =
        (fun n ↦
            have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
            this)
          m →
      n = m
h :
  (fun n ↦
        have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
        this)
      (n + 1) =
    (fun n ↦
        have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
        this)
      0
⊢ n + 1 = 0

case succ.succ
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
hba : b ≠ a
n : ℕ
ih :
  ∀ ⦃m : ℕ⦄,
    (fun n ↦
            have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
            this)
          n =
        (fun n ↦
            have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
            this)
          m →
      n = m
m : ℕ
h :
  (fun n ↦
        have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
        this)
      (n + 1) =
    (fun n ↦
        have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
        this)
      (m + 1)
⊢ n + 1 = m + 1
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 ι
⊢ b.dualBasis.toDual ∘ₗ b.toDual = Dual.eval R M

Tactic:
refine b.ext fun i => b.dualBasis.ext fun j => ?_
  rw [LinearMap.comp_apply, toDual_apply_left, coe_toDual_self, ← coe_dualBasis,
    Dual.eval_apply, Basis.repr_self, Finsupp.single_apply, dualBasis_apply_self]

Goal state after: