mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Localization.Away.Basic

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
P : Type u_3
inst✝¹⁷ : CommSemiring P
x : R
inst✝¹⁶ : Away x S
g : R →+* P
Q : Type u_4
inst✝¹⁵ : CommSemiring Q
inst✝¹⁴ : Algebra P Q
A : Type u_5
inst✝¹³ : CommSemiring A
inst✝¹² : Algebra R A
B : Type u_6
inst✝¹¹ : CommSemiring B
inst✝¹⁰ : Algebra R B
Aₚ : Type u_7
inst✝⁹ : CommSemiring Aₚ
inst✝⁸ : Algebra A Aₚ
inst✝⁷ : Algebra R Aₚ
inst✝⁶ : IsScalarTower R A Aₚ
Bₚ : Type u_8
inst✝⁵ : CommSemiring Bₚ
inst✝⁴ : Algebra B Bₚ
inst✝³ : Algebra R Bₚ
inst✝² : IsScalarTower R B Bₚ
f : A →ₐ[R] B
a : A
inst✝¹ : Away a Aₚ
inst✝ : Away (f a) Bₚ
r : R
⊢ ↑↑(IsLocalization.map Bₚ ↑f ⋯) ((algebraMap R Aₚ) r) = (algebraMap R Bₚ) r

Tactic:
IsScalarTower.algebraMap_apply R A Aₚ,

Goal state after:
R : Type u_1
inst✝²⁰ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝¹⁹ : CommSemiring S
inst✝¹⁸ : Algebra R S
P : Type u_3
inst✝¹⁷ : CommSemiring P
x : R
inst✝¹⁶ : Away x S
g : R →+* P
Q : Type u_4
inst✝¹⁵ : CommSemiring Q
inst✝¹⁴ : Algebra P Q
A : Type u_5
inst✝¹³ : CommSemiring A
inst✝¹² : Algebra R A
B : Type u_6
inst✝¹¹ : CommSemiring B
inst✝¹⁰ : Algebra R B
Aₚ : Type u_7
inst✝⁹ : CommSemiring Aₚ
inst✝⁸ : Algebra A Aₚ
inst✝⁷ : Algebra R Aₚ
inst✝⁶ : IsScalarTower R A Aₚ
Bₚ : Type u_8
inst✝⁵ : CommSemiring Bₚ
inst✝⁴ : Algebra B Bₚ
inst✝³ : Algebra R Bₚ
inst✝² : IsScalarTower R B Bₚ
f : A →ₐ[R] B
a : A
inst✝¹ : Away a Aₚ
inst✝ : Away (f a) Bₚ
r : R
⊢ ↑↑(IsLocalization.map Bₚ ↑f ⋯) ((algebraMap A Aₚ) ((algebraMap R A) r)) = (algebraMap R Bₚ) r
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:
by
    rw [← le_bot_iff, ← SetLike.coe_subset_coe] at h ⊢
    rwa [← coe_jacobson_quotient]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : IsLocalRing R
a b : R
u : Rˣ
hu : ↑u = a + b
⊢ IsUnit a ∨ IsUnit b

Tactic:
← Units.inv_mul_eq_one,

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : IsLocalRing R
a b : R
u : Rˣ
hu : ↑u⁻¹ * (a + b) = 1
⊢ IsUnit a ∨ IsUnit b
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: case refine_1
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
K : Ideal S
J : Ideal R
hJ : J ∈ {J | comap f K ≤ J ∧ J.IsMaximal}
this : comap f (map f J) = J
⊢ J ∈ comap f '' insert ⊤ {J | K ≤ J ∧ J.IsMaximal}

Tactic:
rcases map_eq_top_or_isMaximal_of_surjective _ hf hJ.right with htop | hmax

Goal state after:
case refine_1.inl
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
K : Ideal S
J : Ideal R
hJ : J ∈ {J | comap f K ≤ J ∧ J.IsMaximal}
this : comap f (map f J) = J
htop : map f J = ⊤
⊢ J ∈ comap f '' insert ⊤ {J | K ≤ J ∧ J.IsMaximal}

case refine_1.inr
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
K : Ideal S
J : Ideal R
hJ : J ∈ {J | comap f K ≤ J ∧ J.IsMaximal}
this : comap f (map f J) = J
hmax : (map f J).IsMaximal
⊢ J ∈ comap f '' insert ⊤ {J | K ≤ J ∧ J.IsMaximal}
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: case pos
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
I✝ I : Ideal R
inst✝ : I.IsTwoSided
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
𝔪_mem : 𝔪 ∈ {J | I ≤ J ∧ J.IsMaximal}
r𝔪 : r ∈ 𝔪
⊢ x * r ∈ 𝔪

pp: case neg
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
I✝ I : Ideal R
inst✝ : I.IsTwoSided
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
𝔪_mem : 𝔪 ∈ {J | I ≤ J ∧ J.IsMaximal}
r𝔪 : r ∉ 𝔪
⊢ x * r ∈ 𝔪

Tactic:
· apply 𝔪.smul_mem _ r𝔪

Goal state after:
case neg
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
I✝ I : Ideal R
inst✝ : I.IsTwoSided
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
𝔪_mem : 𝔪 ∈ {J | I ≤ J ∧ J.IsMaximal}
r𝔪 : r ∉ 𝔪
⊢ x * r ∈ 𝔪
Module: Mathlib.RingTheory.Localization.Integer

Goal state before:
pp: case h
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
a : R
b : S
b' : R
hb : (algebraMap R S) b' = b
⊢ (algebraMap R S) a * (algebraMap R S) b' = a • (algebraMap R S) b'

Tactic:
Algebra.smul_def

Goal state after:
case h
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
a : R
b : S
b' : R
hb : (algebraMap R S) b' = b
⊢ (algebraMap R S) a * (algebraMap R S) b' = (algebraMap R S) a * (algebraMap R S) b'
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₁ X₂ Y₂ : Mon C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂), f ⊗ₘ g = f ▷ X₂ ≫ Y₁ ◁ g

Tactic:
intros; ext; simp [tensorHom_def]

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
T : Type u_1
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : IsLocalization S T
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
x✝¹ : R
x✝ : M
⊢ mk (x✝¹ • x✝) 1 = (RingHom.id R) x✝¹ • mk x✝ 1

Tactic:
by simp [mk, OreLocalization.smul_oreDiv]

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
x : Over X
y : Over Y
v : x ⟶ (pullback f).obj y
⊢ (fun u ↦ homMk (pullback.lift (Hom.left u) x.hom ⋯) ⋯) ((fun v ↦ homMk (Hom.left v ≫ pullback.fst y.hom f) ⋯) v) = v

Tactic:
by
            ext
            dsimp
            ext
            · simp
            · simpa using (Over.w v).symm

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
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
map_unit : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
j k : M' →ₗ[R] M''
h : j ∘ₗ f = k ∘ₗ f
⊢ j = k

Tactic:
← lift_unique S f (k.comp f) map_unit j h,

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
map_unit : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
j k : M' →ₗ[R] M''
h : j ∘ₗ f = k ∘ₗ f
⊢ lift S f (k ∘ₗ f) map_unit = k
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
m : M
s : ↥S
⊢ mk' f (s • m) s = f m

Tactic:
delta mk'
  rw [LocalizedModule.mk_cancel, ← mk'_one S f, fromLocalizedModule_mk,
    Module.End.algebraMap_isUnit_inv_apply_eq_iff, OneMemClass.coe_one, mk'_one, one_smul]

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

Goal state before:
pp: R A B X : CommRingCat
f : R ⟶ A
g : R ⟶ B
a : A ⟶ X
b : B ⟶ X
H : IsPushout f g a b
algInst✝¹ : Algebra ↑R ↑A := (Hom.hom f).toAlgebra
algInst✝ : Algebra ↑R ↑B := (Hom.hom g).toAlgebra
e : ↑(of (↑A ⊗[↑R] ↑B)) ≃+* ↑X := (IsPushout.isoIsPushout A B ⋯ H).commRingCatIsoToRingEquiv
⊢ Subring.map (Hom.hom (IsPushout.isoIsPushout A B ⋯ H).inv) ⊤ ≤
    Subring.closure
      (Set.range ⇑(Hom.hom (ofHom Algebra.TensorProduct.includeLeftRingHom)) ∪
        Set.range ⇑(Hom.hom (b ≫ (IsPushout.isoIsPushout A B ⋯ H).inv)))

Tactic:
IsPushout.inr_isoIsPushout_inv,

Goal state after:
R A B X : CommRingCat
f : R ⟶ A
g : R ⟶ B
a : A ⟶ X
b : B ⟶ X
H : IsPushout f g a b
algInst✝¹ : Algebra ↑R ↑A := (Hom.hom f).toAlgebra
algInst✝ : Algebra ↑R ↑B := (Hom.hom g).toAlgebra
e : ↑(of (↑A ⊗[↑R] ↑B)) ≃+* ↑X := (IsPushout.isoIsPushout A B ⋯ H).commRingCatIsoToRingEquiv
⊢ Subring.map (Hom.hom (IsPushout.isoIsPushout A B ⋯ H).inv) ⊤ ≤
    Subring.closure
      (Set.range ⇑(Hom.hom (ofHom Algebra.TensorProduct.includeLeftRingHom)) ∪
        Set.range ⇑(Hom.hom (ofHom ↑Algebra.TensorProduct.includeRight)))
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝¹⁵ : CommSemiring R
S : Submonoid R
M₀ : Type u_6
M₀' : Type u_9
inst✝¹⁴ : AddCommMonoid M₀
inst✝¹³ : AddCommMonoid M₀'
inst✝¹² : Module R M₀
inst✝¹¹ : Module R M₀'
f₀ : M₀ →ₗ[R] M₀'
inst✝¹⁰ : IsLocalizedModule S f₀
M₁ : Type u_7
M₁' : Type u_11
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₁'
inst✝⁷ : Module R M₁
inst✝⁶ : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst✝⁵ : IsLocalizedModule S f₁
M₂ : Type u_8
M₂' : Type u_10
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₂'
inst✝² : Module R M₂
inst✝¹ : Module R M₂'
f₂ : M₂ →ₗ[R] M₂'
inst✝ : IsLocalizedModule S f₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
x : M₀'
⊢ ((map S f₀ f₂) (h ∘ₗ g)) x = ((map S f₁ f₂) h ∘ₗ (map S f₀ f₁) g) x

Tactic:
obtain ⟨⟨x, s⟩, rfl⟩ := IsLocalizedModule.mk'_surjective S f₀ x

Goal state after:
R : Type u_1
inst✝¹⁵ : CommSemiring R
S : Submonoid R
M₀ : Type u_6
M₀' : Type u_9
inst✝¹⁴ : AddCommMonoid M₀
inst✝¹³ : AddCommMonoid M₀'
inst✝¹² : Module R M₀
inst✝¹¹ : Module R M₀'
f₀ : M₀ →ₗ[R] M₀'
inst✝¹⁰ : IsLocalizedModule S f₀
M₁ : Type u_7
M₁' : Type u_11
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₁'
inst✝⁷ : Module R M₁
inst✝⁶ : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst✝⁵ : IsLocalizedModule S f₁
M₂ : Type u_8
M₂' : Type u_10
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₂'
inst✝² : Module R M₂
inst✝¹ : Module R M₂'
f₂ : M₂ →ₗ[R] M₂'
inst✝ : IsLocalizedModule S f₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
x : M₀
s : ↥S
⊢ ((map S f₀ f₂) (h ∘ₗ g)) (Function.uncurry (mk' f₀) (x, s)) =
    ((map S f₁ f₂) h ∘ₗ (map S f₀ f₁) g) (Function.uncurry (mk' f₀) (x, s))
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case map_units.left
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommSemiring R
inst✝³ : Ring S
inst✝² : Ring S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 ↔ ∃ m, m • x = 0
x : ↥M
a b : S'
e : ↑x • a = ↑x • b
⊢ a = b

Tactic:
Algebra.smul_def

Goal state after:
case map_units.left
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommSemiring R
inst✝³ : Ring S
inst✝² : Ring S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 ↔ ∃ m, m • x = 0
x : ↥M
a b : S'
e : (algebraMap R S') ↑x * a = (algebraMap R S') ↑x * b
⊢ a = b
Module: Mathlib.CategoryTheory.ObjectProperty.Opposite

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

Tactic:
exact ⟨i, by rw [hi]⟩

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

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

Tactic:
by
    simpa using hJ I.radical h

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

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

Tactic:
obtain ⟨k, hk⟩ := J.exists_radical_pow_le_of_fg hJ
  exact ⟨k, (pow_right_mono hIJ k).trans hk⟩

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: R : Type w₁
A : Type w₂
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ FinitePresentation R A ↔ ∃ n I x, I.FG

Tactic:
by
  constructor
  · rintro ⟨n, f, hf⟩
    exact ⟨n, RingHom.ker f.toRingHom, Ideal.quotientKerAlgEquivOfSurjective hf.1, hf.2⟩
  · rintro ⟨n, I, e, hfg⟩
    let := (FinitePresentation.mvPolynomial_aux R _).quotient hfg
    exact equiv e

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)
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P

Tactic:
let f : Subtype P → Σ i : Subtype P₁, Subtype (P₂ i.1) := fun c ↦
    ⟨⟨_, hP₁x _ _⟩, _, hP₂y _ c ⟨c.2, hx _ ⟨_, c.2, ⟨.refl _⟩⟩⟩⟩

Goal state after:
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 ⋯, ⋯⟩⟩
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
G : Type u
inst✝ : Groupoid G
F : G ⥤ Type w
p q : F.Elements
f : p ⟶ q
⊢ (ConcreteCategory.hom (F.map ↑f ≫ F.map (Groupoid.inv ↑f))) p.snd = p.snd

Tactic:
by
          rw [← F.map_comp]
          simp

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: case w_base
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X✝ Y✝ : Grothendieck F
f : X✝.Hom Y✝
⊢ (comp X✝.id f).base = f.base

Tactic:
simp [comp, id]

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: case w_fiber
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X✝ Y✝ : Grothendieck F
f : X✝.Hom Y✝
⊢ eqToHom ⋯ ≫ (comp X✝.id f).fiber = f.fiber

Tactic:
simp [comp, id]

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: case w_base
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
f : X.Hom Y
⊢ (comp f Y.id).base = f.base

Tactic:
simp [comp, id]

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

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

Tactic:
map_aeval

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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
inst✝ : IsFilteredOrEmpty C
X Y : D
f g : X ⟶ Y
P : StructuredArrow X F → Prop := fun h ↦ ∃ Z q₁ q₂, h.hom ≫ F.map q₁ = f ≫ Final.homToLift F Y ≫ F.map q₂
h₀ : P (StructuredArrow.mk (f ≫ Final.homToLift F Y))
⊢ ∀ {j₁ j₂ : StructuredArrow X F} (x : j₁ ⟶ j₂), P j₁ → P j₂

Tactic:
rintro U V h ⟨Z, q₁, q₂, hq⟩
      obtain ⟨W, q₃, q₄, hq'⟩ := IsFiltered.span q₁ h.right
      refine ⟨W, q₄, q₂ ≫ q₃, ?_⟩
      rw [F.map_comp, ← reassoc_of% hq, ← F.map_comp, hq', F.map_comp, StructuredArrow.w_assoc]

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
⊢ (i₁ ≫ snd f i) ≫ i = (i₁ ≫ fst f i) ≫ f

Tactic:
simp [condition]

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
⊢ (i₂ ≫ snd f i) ≫ i = (i₂ ≫ fst f i) ≫ f

Tactic:
simp [condition]

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₂
⊢ (i₁ ≫ snd f i) ≫ i = (i₁ ≫ fst f i) ≫ f

Tactic:
simp [condition]

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₂
⊢ (i₂ ≫ snd f i) ≫ i = (i₂ ≫ fst f i) ≫ f

Tactic:
simp [condition]

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
hP : StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ P
hQ : StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ StableUnderComposition fun {R S} [CommRing R] [CommRing S] f ↦ P f ∧ Q f

Tactic:
by
  introv R hf hg
  exact ⟨hP f g hf.1 hg.1, hQ f g hf.2 hg.2⟩

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

Goal state before:
pp: case h₀
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 f g ≫ f) ≫ diagonal i) ≫ fst i i =
    (map f g (f ≫ i) (g ≫ i) (𝟙 X) (𝟙 Y) i ⋯ ⋯ ≫ map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ fst i i

Tactic:
simp [condition]

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

Goal state before:
pp: case h₁
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 f g ≫ f) ≫ diagonal i) ≫ snd i i =
    (map f g (f ≫ i) (g ≫ i) (𝟙 X) (𝟙 Y) i ⋯ ⋯ ≫ map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ snd i i

Tactic:
simp [condition]

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

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
inst✝ : P.IsClosedUnderIsomorphisms
h : P.strictColimitsOfShape J ≤ P
⊢ P.colimitsOfShape J ≤ P

Tactic:
by
    conv_rhs => rw [← P.isoClosure_eq_self]
    rw [← isoClosure_strictColimitsOfShape]
    exact monotone_isoClosure h

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

Goal state before:
pp: case left
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y : C
⊢ tensorHom ℬ (𝟙 X) (𝟙 Y) ≫ (ℬ X Y).cone.π.app { as := WalkingPair.left } =
    𝟙 (tensorObj ℬ X Y) ≫ (ℬ X Y).cone.π.app { as := WalkingPair.left }

Tactic:
simp [tensorHom]

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

Goal state before:
pp: case right
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y : C
⊢ tensorHom ℬ (𝟙 X) (𝟙 Y) ≫ (ℬ X Y).cone.π.app { as := WalkingPair.right } =
    𝟙 (tensorObj ℬ X Y) ≫ (ℬ X Y).cone.π.app { as := WalkingPair.right }

Tactic:
simp [tensorHom]

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

Goal state before:
pp: case left
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ (tensorHom ℬ f₁ f₂ ≫ tensorHom ℬ g₁ g₂) ≫ (ℬ Z₁ Z₂).cone.π.app { as := WalkingPair.left } =
    tensorHom ℬ (f₁ ≫ g₁) (f₂ ≫ g₂) ≫ (ℬ Z₁ Z₂).cone.π.app { as := WalkingPair.left }

Tactic:
simp [tensorHom]

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

Goal state before:
pp: case right
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ (tensorHom ℬ f₁ f₂ ≫ tensorHom ℬ g₁ g₂) ≫ (ℬ Z₁ Z₂).cone.π.app { as := WalkingPair.right } =
    tensorHom ℬ (f₁ ≫ g₁) (f₂ ≫ g₂) ≫ (ℬ Z₁ Z₂).cone.π.app { as := WalkingPair.right }

Tactic:
simp [tensorHom]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ : C
f : X₁ ⟶ X₂
⊢ tensorHom ℬ (𝟙 𝒯.cone.pt) f ≫ (BinaryFan.leftUnitor 𝒯.isLimit (ℬ 𝒯.cone.pt X₂).isLimit).hom =
    (BinaryFan.leftUnitor 𝒯.isLimit (ℬ 𝒯.cone.pt X₁).isLimit).hom ≫ f

Tactic:
simp [tensorHom]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ : C
f : X₁ ⟶ X₂
⊢ tensorHom ℬ f (𝟙 𝒯.cone.pt) ≫ (BinaryFan.rightUnitor 𝒯.isLimit (ℬ X₂ 𝒯.cone.pt).isLimit).hom =
    (BinaryFan.rightUnitor 𝒯.isLimit (ℬ X₁ 𝒯.cone.pt).isLimit).hom ≫ f

Tactic:
simp [tensorHom]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : MonObj B
f g h : A ⟶ B
this : lift (lift f g) h ≫ μ ▷ B ≫ μ = lift (lift f g) h ≫ (α_ B B B).hom ≫ B ◁ μ ≫ μ
⊢ lift (lift f g ≫ μ) h ≫ μ = lift f (lift g h ≫ μ) ≫ μ

Tactic:
rwa [lift_whiskerRight_assoc, lift_lift_associator_hom_assoc, lift_whiskerLeft_assoc] at this

Goal state after: