mathlib-initiative/mathlib-tactics huggingface dataset:
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₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X : ModuleCat R
r : R
g : ↑((restrictScalars f).obj ((coextendScalars f).obj X))
⊢ ((CoextendScalars.equiv f X) (f r • g)) 1 = r • ((CoextendScalars.equiv f X) g) 1

Tactic:
rw [CoextendScalars.smul_apply, one_mul, ← map_smul]

Goal state after:
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X : ModuleCat R
r : R
g : ↑((restrictScalars f).obj ((coextendScalars f).obj X))
⊢ ((CoextendScalars.equiv f X) g) (f r) = ((CoextendScalars.equiv f X) g) (r • 1)
Module: Mathlib.RingTheory.Coalgebra.TensorProduct

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
A : Type u_3
B : Type u_4
inst✝²⁷ : CommSemiring R✝
inst✝²⁶ : CommSemiring S✝
inst✝²⁵ : AddCommMonoid A
inst✝²⁴ : AddCommMonoid B
inst✝²³ : Algebra R✝ S✝
inst✝²² : Module R✝ A
inst✝²¹ : Module S✝ A
inst✝²⁰ : Module R✝ B
inst✝¹⁹ : IsScalarTower R✝ S✝ A
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : CommSemiring S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : AddCommMonoid P
inst✝¹² : AddCommMonoid Q
inst✝¹¹ : Module R M
inst✝¹⁰ : Module R N
inst✝⁹ : Module R P
inst✝⁸ : Module R Q
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower R S M
inst✝⁵ : Coalgebra S M
inst✝⁴ : Module S N
inst✝³ : IsScalarTower R S N
inst✝² : Coalgebra S N
inst✝¹ : Coalgebra R P
inst✝ : Coalgebra R Q
⊢ _root_.TensorProduct.map ↑(_root_.TensorProduct.lid R P) ↑(_root_.TensorProduct.lid R P) ∘ₗ comul =
    comul ∘ₗ ↑(_root_.TensorProduct.lid R P)

Tactic:
ext x
      dsimp
      simp only [one_smul]
      hopf_tensor_induction comul (R := R) x with x₁ x₂
      simp

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O : C
inst✝² : ComonObj M
inst✝¹ : ComonObj N
inst✝ : ComonObj O
A : Comon C
⊢ (Δ ≫ A.X ◁ ε).op = (ρ_ (op A.X)).hom

Tactic:
comul_counit

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O : C
inst✝² : ComonObj M
inst✝¹ : ComonObj N
inst✝ : ComonObj O
A : Comon C
⊢ (ρ_ A.X).inv.op = (ρ_ (op A.X)).hom
Module: Mathlib.CategoryTheory.Monoidal.Comon_

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
M N O : C
inst✝⁶ : ComonObj M
inst✝⁵ : ComonObj N
inst✝⁴ : ComonObj O
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
A : C
inst✝¹ : ComonObj A
F : C ⥤ D
inst✝ : F.OplaxMonoidal
⊢ F.map (Δ ≫ A ◁ ε) ≫ δ F A (𝟙_ C) ≫ F.obj A ◁ η F = F.map (ρ_ A).inv ≫ δ F A (𝟙_ C) ≫ F.obj A ◁ η F

Tactic:
comul_counit

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z : R
h : z ∈ span (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)
⊢ z ∈ span s

Tactic:
refine mem_span_iff.mp h (span s) ?_

Goal state after:
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z : R
h : z ∈ span (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)
⊢ s ∪ s * univ ∪ univ * s ∪ univ * s * univ ⊆ ↑(span s)
Module: Mathlib.RingTheory.Jacobson.Radical

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
m : Ideal R
inst✝ : m.IsMaximal
⊢ sInf {I | I.IsMaximal} ≤ m

Tactic:
exact sInf_le ‹_›

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
h : jacobson (R ⧸ I) = ⊥
⊢ Module.jacobson R (R ⧸ I) = ⊥

Tactic:
← le_bot_iff,

Goal state after:
R : Type u_1
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
h : jacobson (R ⧸ I) ≤ ⊥
⊢ Module.jacobson R (R ⧸ I) ≤ ⊥
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
⊢ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)

Tactic:
IsLocalRing.maximalIdeal_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 ≤ maximalIdeal R
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: 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
n m : ℕ
⊢ selfZPow x B (↑n - ↑m) = mk' B (x ^ n) (Submonoid.pow x m)

Tactic:
by_cases! h : m ≤ n
  · rw [IsLocalization.eq_mk'_iff_mul_eq, Submonoid.pow_apply, Subtype.coe_mk, ← Int.ofNat_sub h,
      selfZPow_natCast, ← map_pow, ← map_mul, ← pow_add, Nat.sub_add_cancel h]
  · rw [← neg_sub, ← Int.ofNat_sub h.le, selfZPow_neg_natCast, IsLocalization.mk'_eq_iff_eq]
    simp [Submonoid.pow_apply, ← pow_add, Nat.sub_add_cancel h.le]

Goal state after:
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 : C
inst✝¹ : MonObj M
inst✝ : MonObj N
⊢ (λ_ (M ⊗ N)).hom = (λ_ (𝟙_ C)).inv ▷ (M ⊗ N) ≫ tensorμ (𝟙_ C) (𝟙_ C) M N ≫ ((λ_ M).hom ⊗ₘ (λ_ N).hom)

Tactic:
exact tensor_left_unitality M N

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

Goal state before:
pp: 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
inst✝ : HasPullback f g
⊢ h.isoPullback.hom ≫ pullback.fst f g = fst

Tactic:
dsimp [isoPullback, cone, CommSq.cone]
  simp

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

Goal state before:
pp: 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
inst✝ : HasPullback f g
⊢ h.isoPullback.hom ≫ pullback.snd f g = snd

Tactic:
dsimp [isoPullback, cone, CommSq.cone]
  simp

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 ↔ IsPushout R T A B

Tactic:
by
  rw [Algebra.IsPushout.comm, Algebra.isPushout_iff, ← isLocalizedModule_iff_isLocalization]
  rw [← isLocalizedModule_iff_isBaseChange (S := S)]

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
α : Type u_7
inst✝ : IsLocalizedModule S f
⊢ IsLocalizedModule S (Finsupp.mapRange.linearMap f)

Tactic:
let e : Localization S ⊗[R] M ≃ₗ[R] M' :=
    (LocalizedModule.equivTensorProduct S M).symm.restrictScalars R ≪≫ₗ IsLocalizedModule.iso S f
  let e' : Localization S ⊗[R] (α →₀ M) ≃ₗ[R] (α →₀ M') :=
    finsuppRight R R (Localization S) M α ≪≫ₗ Finsupp.mapRange.linearEquiv e
  suffices IsLocalizedModule S (e'.symm.toLinearMap ∘ₗ Finsupp.mapRange.linearMap f) by
    convert! this.of_linearEquiv (e := e')
    ext
    simp
  rw [isLocalizedModule_iff_isBaseChange S (Localization S)]
  convert! TensorProduct.isBaseChange R (α →₀ M) (Localization S) using 1
  ext a m
  apply (finsuppRight R R (Localization S) M α).injective
  ext b
  apply e.injective
  suffices (if a = b then f m else 0) = e (1 ⊗ₜ[R] if a = b then m else 0) by
    simpa [e', Finsupp.single_apply, -EmbeddingLike.apply_eq_iff_eq, apply_ite]
  split_ifs with h
  · simp [e]
  · simp only [tmul_zero, map_zero]

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
β : LocalizedModule S M → Prop
h : ∀ (m : M) (s : ↥S), β (mk m s)
⊢ ∀ (x : LocalizedModule S M), β x

Tactic:
rintro ⟨⟨m, s⟩⟩
  exact h m s

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: case refine_1
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₁.pasteHoriz t₂ hi₂)
s : PushoutCocone «i₂» f₂
l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hl' : t₂.inr ≫ l = s.inr
hl : t₁.inl ≫ t₂.inl ≫ l = t₁.inl ≫ s.inl
⊢ («i₂» ≫ t₂.inl) ≫ l = «i₂» ≫ s.inl

Tactic:
t₂.condition,

Goal state after:
case refine_1
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₁.pasteHoriz t₂ hi₂)
s : PushoutCocone «i₂» f₂
l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hl' : t₂.inr ≫ l = s.inr
hl : t₁.inl ≫ t₂.inl ≫ l = t₁.inl ≫ s.inl
⊢ (f₂ ≫ t₂.inr) ≫ l = «i₂» ≫ s.inl
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
Y₃ Y₂ Y₁ X₃ : C
g₂ : Y₃ ⟶ Y₂
g₁ : Y₂ ⟶ Y₁
i₃ : Y₃ ⟶ X₃
t₁✝ : PushoutCocone g₂ i₃
i₂✝ : Y₂ ⟶ t₁✝.pt
t₂✝ : PushoutCocone g₁ i₂✝
hi₂✝ : i₂✝ = t₁✝.inl
t₁ : PushoutCocone g₂ i₃
i₂ : Y₂ ⟶ t₁.pt
t₂ : PushoutCocone g₁ i₂
hi₂ : i₂ = t₁.inl
⊢ g₂ ≫ g₁ ≫ t₂.inl = g₂ ≫ t₁.inl ≫ t₂.inr

Tactic:
t₂.condition,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
Y₃ Y₂ Y₁ X₃ : C
g₂ : Y₃ ⟶ Y₂
g₁ : Y₂ ⟶ Y₁
i₃ : Y₃ ⟶ X₃
t₁✝ : PushoutCocone g₂ i₃
i₂✝ : Y₂ ⟶ t₁✝.pt
t₂✝ : PushoutCocone g₁ i₂✝
hi₂✝ : i₂✝ = t₁✝.inl
t₁ : PushoutCocone g₂ i₃
i₂ : Y₂ ⟶ t₁.pt
t₂ : PushoutCocone g₁ i₂
hi₂ : i₂ = t₁.inl
⊢ g₂ ≫ i₂ ≫ t₂.inr = g₂ ≫ t₁.inl ≫ t₂.inr
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: case refine_3
α : Type u
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hxs : x.IsSupported s
p : α
hps : p ∈ s
n : FreeCommRing α
ih : (map Subtype.val) ((restriction s) n) = n
⊢ (map Subtype.val) ((if H : p ∈ s then of ⟨p, H⟩ else 0) * (restriction s) n) = of p * n

Tactic:
dif_pos hps,

Goal state after:
case refine_3
α : Type u
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hxs : x.IsSupported s
p : α
hps : p ∈ s
n : FreeCommRing α
ih : (map Subtype.val) ((restriction s) n) = n
⊢ (map Subtype.val) (of ⟨p, hps⟩ * (restriction s) n) = of p * n
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x y : T
m : M
s : ↥S
⊢ (x + y) • mk m s = IsLocalization.mk' T ?m.109 ?m.110 • ?m.112

Tactic:
rw [← IsLocalization.mk'_sec (M := S) T x, ← IsLocalization.mk'_sec (M := S) T y,
      ← IsLocalization.mk'_add, IsLocalization.mk'_cancel _ _ s]

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

Goal state before:
pp: R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
T : Type u_1
inst✝⁴ : CommSemiring T
inst✝³ : Algebra R T
inst✝² : IsLocalization S T
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : R
s : ↥S
⊢ IsLocalization.mk' T a s • mk 1 1 = mk ((algebraMap R A) a) s

Tactic:
rw [mk'_smul_mk, Algebra.algebraMap_eq_smul_one, mul_one]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Pullback

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X✝ Y✝ : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst✝¹ : HasPullbacksAlong f
inst✝ : ∀ (Z : C) (g : Z ⟶ Y), Epi (pullback.fst g f)
Z : Over Y
⊢ Epi ((mapPullbackAdj f).counit.app Z)

Tactic:
simp only [Functor.comp_obj, Functor.id_obj, mapPullbackAdj_counit_app]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y✝ : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst✝¹ : HasPullbacksAlong f
inst✝ : ∀ (Z : C) (g : Z ⟶ Y), Epi (pullback.fst g f)
Z : Over Y
⊢ Epi (homMk (pullback.fst Z.hom f) ⋯)
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
M'' : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
l : M' →ₗ[R] M''
hl : l ∘ₗ f = g
⊢ l ∘ₗ ↑(LinearEquiv.refl R M') = l

pp: R : Type u_1
inst✝⁷ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
l : M' →ₗ[R] M''
hl : l ∘ₗ f = g
⊢ (l ∘ₗ ↑(iso S f)) ∘ₗ LocalizedModule.mkLinearMap S M = g

Tactic:
LinearEquiv.refl_toLinearMap,

Goal state after:
R : Type u_1
inst✝⁷ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
l : M' →ₗ[R] M''
hl : l ∘ₗ f = g
⊢ l ∘ₗ LinearMap.id = l

R : Type u_1
inst✝⁷ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
l : M' →ₗ[R] M''
hl : l ∘ₗ f = g
⊢ (l ∘ₗ ↑(iso S f)) ∘ₗ LocalizedModule.mkLinearMap S M = g
Module: Mathlib.CategoryTheory.Limits.Comma

Goal state before:
pp: J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
F : J ⥤ Comma L R
inst✝ : PreservesLimit (F ⋙ snd L R) R
c₁ : Cone (F ⋙ fst L R)
c₂ : Cone (F ⋙ snd L R)
t₂ : IsLimit c₂
j₁ j₂ : J
t : j₁ ⟶ j₂
⊢ ((const J).obj { left := c₁.pt, right := c₂.pt, hom := (isLimitOfPreserves R t₂).lift (limitAuxiliaryCone F c₁) }).map
        t ≫
      { left := c₁.π.app j₂, right := c₂.π.app j₂, w := ⋯ } =
    { left := c₁.π.app j₁, right := c₂.π.app j₁, w := ⋯ } ≫ F.map t

Tactic:
ext
        · simp [← c₁.w t]
        · simp [← c₂.w t]

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

Goal state before:
pp: J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
F : J ⥤ Comma L R
inst✝ : PreservesColimit (F ⋙ fst L R) L
c₁ : Cocone (F ⋙ fst L R)
t₁ : IsColimit c₁
c₂ : Cocone (F ⋙ snd L R)
j₁ j₂ : J
t : j₁ ⟶ j₂
⊢ F.map t ≫ { left := c₁.ι.app j₂, right := c₂.ι.app j₂, w := ⋯ } =
    { left := c₁.ι.app j₁, right := c₂.ι.app j₁, w := ⋯ } ≫
      ((const J).obj
            { left := c₁.pt, right := c₂.pt,
              hom := (isColimitOfPreserves L t₁).desc (colimitAuxiliaryCocone F c₂) }).map
        t

Tactic:
ext
        · simp [← c₁.w t]
        · simp [← c₂.w t]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
P : ObjectProperty C
Q : ObjectProperty D
e : C ≌ D
inst✝ : Q.IsClosedUnderIsomorphisms
h : Q.inverseImage e.functor = P
x✝ : P.FullSubcategory
X : C
hX : P X
⊢ Q ((P.ι ⋙ e.functor).obj { obj := X, property := hX })

Tactic:
rwa [← h] at hX

Goal state after:
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
F : C ⥤ D
H₁ : ObjectProperty.EssentiallySmall.{w, v', u'} (P.map F)
H₂ : ∀ (Y : D), ObjectProperty.EssentiallySmall.{w, v, u} (P ⊓ fun x ↦ Nonempty (F.obj x ≅ Y))
P₁ : ObjectProperty D
hP₁ : ObjectProperty.Small.{w, v', u'} P₁
x : (i : D) → P.map F i → D
hP₁x : ∀ (i : D) (a : P.map F i), P₁ (x i a)
hx : ∀ (i : D) (a : P.map F i), Nonempty (i ≅ x i a)
P₂ : D → ObjectProperty C
hP₂ : ∀ (Y : D), ObjectProperty.Small.{w, v, u} (P₂ Y)
y : (Y : D) → (i : C) → (P ⊓ fun x ↦ Nonempty (F.obj x ≅ Y)) i → C
hP₂y : ∀ (Y : D) (i : C) (a : (P ⊓ fun x ↦ Nonempty (F.obj x ≅ Y)) i), P₂ Y (y Y i a)
hy : ∀ (Y : D) (i : C) (a : (P ⊓ fun x ↦ Nonempty (F.obj x ≅ Y)) i), Nonempty (i ≅ y Y i a)
f : Subtype P → (i : Subtype P₁) × Subtype (P₂ ↑i) := fun c ↦ ⟨⟨x (F.obj ↑c) ⋯, ⋯⟩, ⟨y (x (F.obj ↑c) ⋯) ↑c ⋯, ⋯⟩⟩
g : (i : Subtype P₁) × Subtype (P₂ ↑i) → C := fun i ↦ ↑i.snd
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P

Tactic:
exact ⟨.ofObj g, inferInstance, fun X hX ↦ ⟨_, ⟨f ⟨X, hX⟩⟩, hy _ _ _⟩⟩

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
E : Type u_1
inst✝ : Category.{v_1, u_1} E
fib : (c : C) → ↑(F.obj c) ⥤ E
hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ (F.map f).toFunctor ⋙ fib c'
hom_id : ∀ (c : C), hom (𝟙 c) = eqToHom (@_proof_145 C inst✝² F E inst✝ fib c)
hom_comp :
  ∀ (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃),
    hom (f ≫ g) =
      hom f ≫ (F.map f).toFunctor.whiskerLeft (hom g) ≫ eqToHom (@_proof_146 C inst✝² F E inst✝ fib c₁ c₂ c₃ f g)
X✝ Y✝ Z✝ : Grothendieck F
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (hom (f ≫ g).base).app X✝.fiber ≫ (fib Z✝.base).map (f ≫ g).fiber =
    ((hom f.base).app X✝.fiber ≫ (fib Y✝.base).map f.fiber) ≫ (hom g.base).app Y✝.fiber ≫ (fib Z✝.base).map g.fiber

Tactic:
by simp [hom_comp]

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

Goal state before:
pp: case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
s : Cocone (F ⋙ G)
j : C
⊢ ∀ (X₁ X₂ : C) (k₁ : F.obj j ⟶ F.obj X₁) (k₂ : F.obj j ⟶ F.obj X₂) (f : X₁ ⟶ X₂),
    k₁ ≫ F.map f = k₂ → G.map k₁ ≫ s.ι.app X₁ = s.ι.app j → G.map k₂ ≫ s.ι.app X₂ = s.ι.app j

Tactic:
intro j₁ j₂ k₁ k₂ f w h
    rw [← w]
    rw [← s.w f] at h
    simpa using! h

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

Goal state before:
pp: case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Initial
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cone (F ⋙ G)
X : C
Y : D
f : F.obj X ⟶ Y
⊢ ∀ (X₁ X₂ : C) (k₁ : F.obj X₁ ⟶ Y) (k₂ : F.obj X₂ ⟶ Y) (f_1 : X₁ ⟶ X₂),
    F.map f_1 ≫ k₂ = k₁ → c.π.app X₁ ≫ G.map k₁ = c.π.app X ≫ G.map f → c.π.app X₂ ≫ G.map k₂ = c.π.app X ≫ G.map f

Tactic:
intro _ _ _ _ _ h₁ h₂
    simp [← h₂, ← h₁, ← Functor.comp_map]

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
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
        fst (i₁ ≫ snd f i) (i₂ ≫ snd f i)) ≫
      i₁ =
    (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
        snd (i₁ ≫ snd f i) (i₂ ≫ snd f i)) ≫
      i₂

Tactic:
ext
  · simp only [Category.assoc, pullback_diagonal_map_snd_fst_fst,
      pullback_diagonal_map_snd_snd_fst]
  · simp only [Category.assoc, condition]

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 : 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
e : R' →+* S' := (↑e₂).comp ((IsLocalization.map (Localization.Away (f r)) f ⋯).comp ↑e₁)
this : e = IsLocalization.Away.map R' S' f r
⊢ (CommRingCat.Hom.hom e₂.toCommRingCatIso.hom).comp
      (CommRingCat.Hom.hom
        (CommRingCat.ofHom
          {
            toFun := fun x ↦
              (CommRingCat.Hom.hom
                  (CommRingCat.ofHom
                    {
                      toFun :=
                        (↑((IsLocalization.toLocalizationMap (Submonoid.powers r) (Localization.Away r)).lift₀
                              ((algebraMap S (Localization.Away (f r))).comp f).toMonoidWithZeroHom ⋯)).toFun,
                      map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }))
                ((CommRingCat.Hom.hom e₁.toCommRingCatIso.hom) x),
            map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ })) =
    IsLocalization.Away.map R' S' f r

Tactic:
by
    convert! this

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
⊢ P.strictLimitsOfShape J ≤ P.limitsOfShape J

Tactic:
rintro X ⟨F, hF⟩
  exact ⟨.limit F hF⟩

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
inst✝ : W.IsStableUnderColimitsOfShape J
⊢ W.colimitsOfShape J ≤ W

Tactic:
← isStableUnderColimitsOfShape_iff_colimitsOfShape_le

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
inst✝ : W.IsStableUnderColimitsOfShape J
⊢ W.IsStableUnderColimitsOfShape J
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case refine_2.hg
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
P : MorphismProperty C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
Q : MorphismProperty C
inst✝ : Q.IsStableUnderBaseChange
hP : Q ≤ P.diagonal
Y X S : C
g : Y ⟶ X
f : X ⟶ S
hf : Q f
hcomp : P (g ≫ f)
gr : Y ⟶ pullback (g ≫ f) f := ⋯
this : g = gr ≫ pullback.snd (g ≫ f) f
⊢ P (pullback.snd (g ≫ f) f)

Tactic:
· exact P.pullback_snd _ _ hcomp

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
f₁ f₂ f₃ : X ⟶ M
⊢ lift f₁ (lift f₂ f₃) ≫ M ◁ μ ≫ μ = lift f₁ (lift f₂ f₃ ≫ μ) ≫ μ

Tactic:
← id_tensorHom,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
f₁ f₂ f₃ : X ⟶ M
⊢ lift f₁ (lift f₂ f₃) ≫ (𝟙 M ⊗ₘ μ) ≫ μ = lift f₁ (lift f₂ f₃ ≫ μ) ≫ μ