mathlib-initiative/mathlib-tactics huggingface dataset:
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
f : A ⟶ trivial C
⊢ f.hom ≫ ε = ε

Tactic:
IsComonHom.hom_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
f : A ⟶ trivial C
⊢ ε = ε
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
⊢ ε.op ▷ op A.X ≫ Δ.op = (λ_ (op A.X)).hom

Tactic:
rw [← op_whiskerRight, ← op_comp, counit_comul]
    rfl

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
inj : Function.Injective ⇑f
h : jacobson R₂ M₂ = ⊥
⊢ comap f (jacobson R₂ M₂) ≤ ⊥

Tactic:
h,

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
inj : Function.Injective ⇑f
h : jacobson R₂ M₂ = ⊥
⊢ comap f ⊥ ≤ ⊥
Module: Mathlib.RingTheory.Jacobson.Radical

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

Tactic:
h,

Goal state after:
R : Type u_1
inst✝² : Ring R
ι : Type u_6
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommGroup (M i)
inst✝ : (i : ι) → Module R (M i)
h : ∀ (i : ι), jacobson R (M i) = ⊥
⊢ (pi Set.univ fun x ↦ ⊥) ≤ ⊥
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Ring R
s : Set R
z : R
⊢ ∀ (y x : R), y ∈ univ * s * univ → y * x ∈ univ * s * univ

Tactic:
· rintro - x ⟨y, hy, r, -, rfl⟩
      exact ⟨y, hy, r * x, mem_univ _, (mul_assoc ..).symm⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
I I' : TwoSidedIdeal R
⊢ { toFun := fun I ↦ ⟨asIdeal I, ⋯⟩,
          invFun := fun I ↦
            have this := ⋯;
            (↑I).toTwoSided,
          left_inv := ⋯, right_inv := ⋯ }
        I ≤
      { toFun := fun I ↦ ⟨asIdeal I, ⋯⟩,
          invFun := fun I ↦
            have this := ⋯;
            (↑I).toTwoSided,
          left_inv := ⋯, right_inv := ⋯ }
        I' ↔
    I ≤ I'

Tactic:
simp [SetLike.le_def]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
K : Type u_3
inst✝ : Field K
a : K
h : a = 0
⊢ IsUnit (1 - a)

Tactic:
h,

Goal state after:
R : Type u_1
S : Type u_2
K : Type u_3
inst✝ : Field K
a : K
h : a = 0
⊢ IsUnit (1 - 0)
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: case refine_2
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
K J : Ideal S
hJ : J ∈ {J | K ≤ J ∧ J.IsMaximal}
this : J.IsMaximal
⊢ sInf {J | comap f K ≤ J ∧ J.IsMaximal} ≤ comap f J

Tactic:
exact sInf_le ⟨comap_mono hJ.left, comap_isMaximal_of_surjective _ hf⟩

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Finset R
f : (a : ↑↑s) → Away ↑a
h : ∀ (a b : ↑↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)
mem : 1 ∈ Ideal.span ↑s
span_eq : Ideal.span ↑s = ⊤
n : ↑↑s → ℕ
r✝ : ↑↑s → R
eq✝ : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) ↑a ^ n a = (algebraMap R (Away ↑a)) (r✝ a)
N : ℕ := s.attach.sup n
r : ↑↑s → R := fun a ↦ ↑a ^ (N - n a) * r✝ a
eq : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) (↑a ^ N) = (algebraMap R (Away ↑a)) (r a)
a b : ↑↑s
⊢ (Away.awayToAwayRight ↑a ↑b) (f a) * (algebraMap R (Away (↑a * ↑b))) (↑a ^ N) *
      (algebraMap R (Away (↑a * ↑b))) (↑b ^ N) =
    (Away.awayToAwayLeft ↑b ↑a) (f b) * (algebraMap R (Away (↑a * ↑b))) (↑b ^ N) *
      (algebraMap R (Away (↑a * ↑b))) (↑a ^ N)

Tactic:
h,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
s : Finset R
f : (a : ↑↑s) → Away ↑a
h : ∀ (a b : ↑↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)
mem : 1 ∈ Ideal.span ↑s
span_eq : Ideal.span ↑s = ⊤
n : ↑↑s → ℕ
r✝ : ↑↑s → R
eq✝ : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) ↑a ^ n a = (algebraMap R (Away ↑a)) (r✝ a)
N : ℕ := s.attach.sup n
r : ↑↑s → R := fun a ↦ ↑a ^ (N - n a) * r✝ a
eq : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) (↑a ^ N) = (algebraMap R (Away ↑a)) (r a)
a b : ↑↑s
⊢ (Away.awayToAwayLeft ↑b ↑a) (f b) * (algebraMap R (Away (↑a * ↑b))) (↑a ^ N) *
      (algebraMap R (Away (↑a * ↑b))) (↑b ^ N) =
    (Away.awayToAwayLeft ↑b ↑a) (f b) * (algebraMap R (Away (↑a * ↑b))) (↑b ^ N) *
      (algebraMap R (Away (↑a * ↑b))) (↑a ^ N)
Module: Mathlib.RingTheory.LocalRing.RingHom.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : IsLocalRing S
f : R →+* S
inst✝ : IsLocalHom f
a b : R
h : a + b = 1
⊢ f (a + b) = 1

Tactic:
h,

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : IsLocalRing S
f : R →+* S
inst✝ : IsLocalHom f
a b : R
h : a + b = 1
⊢ f 1 = 1
Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial

Goal state before:
pp: case neg.refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j : J
h_1 : ¬j = i
f : j ⟶ i
this : IsIso (F.map f)
⊢ ((Functor.const J).obj (F.1 i)).map f ≫ eqToHom ⋯ = (H j h_1).from (((Functor.const J).obj (F.1 i)).obj j) ≫ F.map f

Tactic:
← IsIso.comp_inv_eq

Goal state after:
case neg.refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j : J
h_1 : ¬j = i
f : j ⟶ i
this : IsIso (F.map f)
⊢ (((Functor.const J).obj (F.1 i)).map f ≫ eqToHom ⋯) ≫ inv (F.map f) =
    (H j h_1).from (((Functor.const J).obj (F.1 i)).obj j)
Module: Mathlib.RingTheory.Localization.Integer

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

Tactic:
exact Set.mem_image_of_mem _ x.prop

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

Goal state before:
pp: case e_6
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_3
Mₛ : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid Mₛ
inst✝¹ : Module R Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
v : ι → M
hv : LinearIndependent R v
h : ∀ (s : ↥S), IsRegular ↑s
w✝¹ w✝ : ι →₀ R
eq✝ : f ((Finsupp.linearCombination R v) w✝¹) = f ((Finsupp.linearCombination R v) w✝)
i : ι
s : ↥S
eq : s • (Finsupp.linearCombination R v) w✝¹ = s • (Finsupp.linearCombination R v) w✝
⊢ w✝¹ i = w✝ i

Tactic:
simp_rw [Submonoid.smul_def, ← map_smul] at eq

Goal state after:
case e_6
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_3
Mₛ : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid Mₛ
inst✝¹ : Module R Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
v : ι → M
hv : LinearIndependent R v
h : ∀ (s : ↥S), IsRegular ↑s
w✝¹ w✝ : ι →₀ R
eq✝ : f ((Finsupp.linearCombination R v) w✝¹) = f ((Finsupp.linearCombination R v) w✝)
i : ι
s : ↥S
eq : (Finsupp.linearCombination R v) (↑s • w✝¹) = (Finsupp.linearCombination R v) (↑s • w✝)
⊢ w✝¹ i = w✝ i
Module: Mathlib.RingTheory.Localization.BaseChange

Goal state before:
pp: R : Type u_10
inst✝² : CommRing R
M : Submonoid R
S : Type u_12
inst✝¹ : CommRing S
inst✝ : Algebra R S
Rₘ : Type u_10 := Localization M
Sₘ : Type u_12 := Localization (Algebra.algebraMapSubmonoid S M)
x : R
y : ↥M
this : Algebra Rₘ (S ⊗[R] Rₘ) := Algebra.TensorProduct.rightAlgebra
h1 : 1 ⊗ₜ[R] IsLocalization.mk' Rₘ x y = (algebraMap Rₘ (S ⊗[R] Rₘ)) (IsLocalization.mk' Rₘ x y)
h : ∀ (x : R), (algebraMap S Sₘ) ((algebraMap R S) x) = (algebraMap Rₘ Sₘ) ((algebraMap R Rₘ) x)
⊢ (algebraMap S (Localization (Algebra.algebraMapSubmonoid S M))) ((algebraMap R S) x) =
    (algebraMap (Localization M) (Localization (Algebra.algebraMapSubmonoid S M)))
        (IsLocalization.mk' (Localization M) x y) *
      (algebraMap S (Localization (Algebra.algebraMapSubmonoid S M))) ((algebraMap R S) ↑y)

Tactic:
h,

Goal state after:
R : Type u_10
inst✝² : CommRing R
M : Submonoid R
S : Type u_12
inst✝¹ : CommRing S
inst✝ : Algebra R S
Rₘ : Type u_10 := Localization M
Sₘ : Type u_12 := Localization (Algebra.algebraMapSubmonoid S M)
x : R
y : ↥M
this : Algebra Rₘ (S ⊗[R] Rₘ) := Algebra.TensorProduct.rightAlgebra
h1 : 1 ⊗ₜ[R] IsLocalization.mk' Rₘ x y = (algebraMap Rₘ (S ⊗[R] Rₘ)) (IsLocalization.mk' Rₘ x y)
h : ∀ (x : R), (algebraMap S Sₘ) ((algebraMap R S) x) = (algebraMap Rₘ Sₘ) ((algebraMap R Rₘ) x)
⊢ (algebraMap Rₘ Sₘ) ((algebraMap R Rₘ) x) =
    (algebraMap (Localization M) (Localization (Algebra.algebraMapSubmonoid S M)))
        (IsLocalization.mk' (Localization M) x y) *
      (algebraMap S (Localization (Algebra.algebraMapSubmonoid S M))) ((algebraMap R S) ↑y)
Module: Mathlib.RingTheory.Localization.BaseChange

Goal state before:
pp: R : Type u_10
inst✝² : CommRing R
M : Submonoid R
S : Type u_12
inst✝¹ : CommRing S
inst✝ : Algebra R S
Rₘ : Type u_10 := Localization M
Sₘ : Type u_12 := Localization (Algebra.algebraMapSubmonoid S M)
x : R
y : ↥M
this : Algebra Rₘ (S ⊗[R] Rₘ) := Algebra.TensorProduct.rightAlgebra
h1 : 1 ⊗ₜ[R] IsLocalization.mk' Rₘ x y = (algebraMap Rₘ (S ⊗[R] Rₘ)) (IsLocalization.mk' Rₘ x y)
h : ∀ (x : R), (algebraMap S Sₘ) ((algebraMap R S) x) = (algebraMap Rₘ Sₘ) ((algebraMap R Rₘ) x)
⊢ (algebraMap Rₘ Sₘ) ((algebraMap R Rₘ) x) =
    (algebraMap (Localization M) (Localization (Algebra.algebraMapSubmonoid S M)))
        (IsLocalization.mk' (Localization M) x y) *
      (algebraMap S (Localization (Algebra.algebraMapSubmonoid S M))) ((algebraMap R S) ↑y)

Tactic:
h,

Goal state after:
R : Type u_10
inst✝² : CommRing R
M : Submonoid R
S : Type u_12
inst✝¹ : CommRing S
inst✝ : Algebra R S
Rₘ : Type u_10 := Localization M
Sₘ : Type u_12 := Localization (Algebra.algebraMapSubmonoid S M)
x : R
y : ↥M
this : Algebra Rₘ (S ⊗[R] Rₘ) := Algebra.TensorProduct.rightAlgebra
h1 : 1 ⊗ₜ[R] IsLocalization.mk' Rₘ x y = (algebraMap Rₘ (S ⊗[R] Rₘ)) (IsLocalization.mk' Rₘ x y)
h : ∀ (x : R), (algebraMap S Sₘ) ((algebraMap R S) x) = (algebraMap Rₘ Sₘ) ((algebraMap R Rₘ) x)
⊢ (algebraMap Rₘ Sₘ) ((algebraMap R Rₘ) x) =
    (algebraMap (Localization M) (Localization (Algebra.algebraMapSubmonoid S M)))
        (IsLocalization.mk' (Localization M) x y) *
      (algebraMap Rₘ Sₘ) ((algebraMap R Rₘ) ↑y)
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
g : A
B : Type u_10
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R B
inst✝² : Algebra A B
inst✝¹ : IsScalarTower R A B
inst✝ : Away g B
⊢ IsLocalization (Submonoid.map Algebra.TensorProduct.includeRight (Submonoid.powers g)) (Localization.Away (1 ⊗ₜ[R] g))

Tactic:
by
    simp only [Submonoid.map_powers, Algebra.TensorProduct.includeRight_apply]
    infer_instance

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

Goal state before:
pp: R : Type u_7
S : Type u_8
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring S
inst✝⁷ : Algebra R S
A : Type u_9
inst✝⁶ : CommSemiring A
inst✝⁵ : Algebra R A
g : A
B : Type u_10
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R B
inst✝² : Algebra A B
inst✝¹ : IsScalarTower R A B
inst✝ : Away g B
x : S
a : A
⊢ IsLocalization (Submonoid.map Algebra.TensorProduct.includeRight (Submonoid.powers g)) (Localization.Away (1 ⊗ₜ[R] g))

Tactic:
by
    simp only [Submonoid.map_powers, Algebra.TensorProduct.includeRight_apply]
    infer_instance

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: case h
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun x ↦ x ∈ s
x : FreeCommRing α
hx : x.IsSupported s
z : α
hzs : z ∈ s
n✝ : FreeCommRing α
a✝ : ∃ n, (lift fun a ↦ if a ∈ s then 0 else X) n✝ = ↑n
⊢ (lift fun a ↦ if a ∈ s then 0 else X) (of z) * (lift fun a ↦ if a ∈ s then 0 else X) n✝ = ↑0

Tactic:
lift_of,

Goal state after:
case h
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun x ↦ x ∈ s
x : FreeCommRing α
hx : x.IsSupported s
z : α
hzs : z ∈ s
n✝ : FreeCommRing α
a✝ : ∃ n, (lift fun a ↦ if a ∈ s then 0 else X) n✝ = ↑n
⊢ (if z ∈ s then 0 else X) * (lift fun a ↦ if a ∈ s then 0 else X) n✝ = ↑0
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''
A : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Module A M'
inst✝⁴ : IsLocalization S A
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
inst✝ : IsScalarTower R A M'
f : M →ₗ[R] M'
g✝ g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
m✝ : LocalizedModule S M
x✝² x✝¹ : M × ↥S
m : M
s : ↥S
m' : M
s' : ↥S
x✝ : (m, s) ≈ (m', s')
c : ↥S
eq1 : ↑c • ↑s' • m = ↑c • ↑s • m'
this✝ : c • s • g m' = c • s' • g m
this : Function.Injective ⇑⋯.unit.inv
⊢ ↑⋯.unit⁻¹ (↑c • ↑(m', s').2 • g m) = ↑(m, s).2 • g m'

Tactic:
rw [Module.End.algebraMap_isUnit_inv_apply_eq_iff, ← g.map_smul, ← g.map_smul, ← g.map_smul, ←
      g.map_smul, eq1]

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

Goal state before:
pp: R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : PushoutCocone (ofHom (algebraMap R A)) (ofHom (algebraMap R B))
this : Algebra R ↑s.pt := ((Hom.hom s.inl).comp (algebraMap R A)).toAlgebra
f' : A →ₐ[R] ↑s.pt :=
  let __src := Hom.hom s.inl;
  { toRingHom := __src, commutes' := ⋯ }
g' : B →ₐ[R] ↑s.pt :=
  let __src := Hom.hom s.inr;
  { toRingHom := __src, commutes' := ⋯ }
⊢ { l //
    (pushoutCocone R A B).inl ≫ l = s.inl ∧
      (pushoutCocone R A B).inr ≫ l = s.inr ∧
        ∀ {m : (pushoutCocone R A B).pt ⟶ s.pt},
          (pushoutCocone R A B).inl ≫ m = s.inl → (pushoutCocone R A B).inr ≫ m = s.inr → m = l }

Tactic:
letI : Algebra R (pushoutCocone R A B).pt := show Algebra R (A ⊗[R] B) by infer_instance

Goal state after:
R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : PushoutCocone (ofHom (algebraMap R A)) (ofHom (algebraMap R B))
this✝ : Algebra R ↑s.pt := ((Hom.hom s.inl).comp (algebraMap R A)).toAlgebra
f' : A →ₐ[R] ↑s.pt :=
  let __src := Hom.hom s.inl;
  { toRingHom := __src, commutes' := ⋯ }
g' : B →ₐ[R] ↑s.pt :=
  let __src := Hom.hom s.inr;
  { toRingHom := __src, commutes' := ⋯ }
this : Algebra R ↑(pushoutCocone R A B).pt :=
  have this := inferInstance;
  this
⊢ { l //
    (pushoutCocone R A B).inl ≫ l = s.inl ∧
      (pushoutCocone R A B).inr ≫ l = s.inr ∧
        ∀ {m : (pushoutCocone R A B).pt ⟶ s.pt},
          (pushoutCocone R A B).inl ≫ m = s.inl → (pushoutCocone R A B).inr ≫ m = s.inr → m = l }
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)
⊢ (LocalizedModule.lift S g h ∘ₗ ↑(iso S f).symm) ∘ₗ f = g

Tactic:
rw [LinearMap.comp_assoc, iso_symm_comp, LocalizedModule.lift_comp S g h]

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

Goal state before:
pp: J : Type u'
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
r : ↑c.pt
inv : (j : J) → ↑(F.obj j)
h_inv : ∀ (j : J), (ConcreteCategory.hom (c.π.app j)) r * inv j = 1
j k : J
f : j ⟶ k
h : (ConcreteCategory.hom (c.π.app k)) r * (ConcreteCategory.hom (F.map f)) (inv j) = 1
this : (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (c.π.app j)) r) = (ConcreteCategory.hom (c.π.app k)) r
⊢ (ConcreteCategory.hom (c.π.app k)) r * (ConcreteCategory.hom (F.map f)) (inv j) * inv k = inv k

Tactic:
h,

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

Goal state before:
pp: J : Type u'
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
j : J
hj :
  ∀ (x : ↑c.pt),
    IsUnit ((ConcreteCategory.hom (c.π.app j)) x) →
      ∀ (i : J),
        ∃ k f g,
          IsLocalHom (Hom.hom (F.map f)) ∧
            (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (c.π.app i)) x) =
              (ConcreteCategory.hom (F.map g)) ((ConcreteCategory.hom (c.π.app j)) x)
x : ↑c.pt
hx : IsUnit ((Hom.hom (c.π.app j)) x)
⊢ IsUnit x

Tactic:
rw [isUnit_iff_forall_isUnit F hc]

Goal state after:
J : Type u'
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
j : J
hj :
  ∀ (x : ↑c.pt),
    IsUnit ((ConcreteCategory.hom (c.π.app j)) x) →
      ∀ (i : J),
        ∃ k f g,
          IsLocalHom (Hom.hom (F.map f)) ∧
            (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (c.π.app i)) x) =
              (ConcreteCategory.hom (F.map g)) ((ConcreteCategory.hom (c.π.app j)) x)
x : ↑c.pt
hx : IsUnit ((Hom.hom (c.π.app j)) x)
⊢ ∀ (j : J), IsUnit ((ConcreteCategory.hom (c.π.app j)) x)
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: A B : CommRingCat
f g : A ⟶ B
x : ↑A
e : x ∈ (Hom.hom f).eqLocus (Hom.hom g)
⊢ (Hom.hom (ofHom ((Hom.hom f).eqLocus (Hom.hom g)).subtype ≫ f)) ⟨x, e⟩ =
    (Hom.hom (ofHom ((Hom.hom f).eqLocus (Hom.hom g)).subtype ≫ g)) ⟨x, e⟩

Tactic:
simpa using e

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.map₂Iso (λ_ f)).inv = F.mapId a ▷ F.map f ≫ F.mapComp (𝟙 a) f

Tactic:
← 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₂Iso (ρ_ f)).inv = F.map f ◁ F.mapId b ≫ F.mapComp f (𝟙 b)

Tactic:
← 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.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
inst✝ : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
h : ((↑e).comp f).toRingHom = (↑e).comp f.toRingHom
h1 : ↑e.toRingEquiv = (↑e).toRingHom
⊢ ((↑e).comp f).toRingHom = (↑e.toRingEquiv).comp f.toRingHom

Tactic:
h,

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
inst✝ : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
h : ((↑e).comp f).toRingHom = (↑e).comp f.toRingHom
h1 : ↑e.toRingEquiv = (↑e).toRingHom
⊢ (↑e).comp f.toRingHom = (↑e.toRingEquiv).comp f.toRingHom
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✝¹ : LocallySmall.{w, v, u} C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : P ≤ Q.isoClosure
this : (ιOfLE h₁).IsEquivalence
⊢ EssentiallySmall.{w, v, u} P.FullSubcategory

Tactic:
rw [← essentiallySmall_congr (ιOfLE h₁).asEquivalence]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
P : ObjectProperty C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : P ≤ Q.isoClosure
this : (ιOfLE h₁).IsEquivalence
⊢ EssentiallySmall.{w, v, u} Q.FullSubcategory
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F G : C ⥤ D
η : F ⟶ G
⊢ ∀ ⦃X Y : WithInitial C⦄ (f : X ⟶ Y),
    ((map F).map f ≫
        match Y with
        | of x => η.app x
        | star => 𝟙 star) =
      (match X with
        | of x => η.app x
        | star => 𝟙 star) ≫
        (map G).map f

Tactic:
intro X Y f
    match X, Y, f with
    | of x, of y, f => exact η.naturality f
    | star, of x, _ => rfl
    | star, star, _ => rfl

Goal state after: