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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
A : n → Type u_3
inst✝² : (i : n) → AddCommMonoid (A i)
inst✝¹ : (i : n) → Module R (A i)
inst✝ : (i : n) → Coalgebra R (A i)
i✝ : n
⊢ ↑(TensorProduct.assoc R ((i : n) → A i) ((i : n) → A i) ((i : n) → A i)) ∘ₗ
      map (map (LinearMap.single R A i✝) (LinearMap.single R A i✝)) (LinearMap.single R A i✝) ∘ₗ
        rTensor (A i✝) comul ∘ₗ comul =
    map (LinearMap.single R A i✝) (map (LinearMap.single R A i✝) (LinearMap.single R A i✝)) ∘ₗ
      ↑(TensorProduct.assoc R (A i✝) (A i✝) (A i✝)) ∘ₗ rTensor (A i✝) comul ∘ₗ comul

Tactic:
← comp_assoc comul,

Goal state after:
R : Type u_1
n : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
A : n → Type u_3
inst✝² : (i : n) → AddCommMonoid (A i)
inst✝¹ : (i : n) → Module R (A i)
inst✝ : (i : n) → Coalgebra R (A i)
i✝ : n
⊢ (↑(TensorProduct.assoc R ((i : n) → A i) ((i : n) → A i) ((i : n) → A i)) ∘ₗ
        map (map (LinearMap.single R A i✝) (LinearMap.single R A i✝)) (LinearMap.single R A i✝) ∘ₗ
          rTensor (A i✝) comul) ∘ₗ
      comul =
    (map (LinearMap.single R A i✝) (map (LinearMap.single R A i✝) (LinearMap.single R A i✝)) ∘ₗ
        ↑(TensorProduct.assoc R (A i✝) (A i✝) (A i✝)) ∘ₗ rTensor (A i✝) comul) ∘ₗ
      comul
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
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : S
g : ↑((restrictScalars f).obj (of S S)) →ₗ[R] M
x y : S
⊢ g ((x + y) * s) = g (x * s) + g (y * s)

Tactic:
add_mul,

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
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : S
g : ↑((restrictScalars f).obj (of S S)) →ₗ[R] M
x y : S
⊢ g (x * s + y * s) = g (x * s) + g (y * s)
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R : Type u₁
inst✝ : CommRing R
M : ModuleCat R
m : ↑M
⊢ (ConcreteCategory.hom ((extendScalarsId R).hom.app M)) (1 ⊗ₜ[R] m) = m

Tactic:
rw [← extendRestrictScalarsAdj_homEquiv_apply,
    homEquiv_extendScalarsId]

Goal state after:
R : Type u₁
inst✝ : CommRing R
M : ModuleCat R
m : ↑M
⊢ (ConcreteCategory.hom ((restrictScalarsId R).inv.app M)) m = m
Module: Mathlib.Algebra.Ring.BooleanRing

Goal state before:
pp: α : Type u_1
inst✝ : BooleanRing α
a : α
⊢ (a + a) * (a + a) = a * a + a * a + (a * a + a * a)

Tactic:
add_mul,

Goal state after:
α : Type u_1
inst✝ : BooleanRing α
a : α
⊢ a * (a + a) + a * (a + a) = a * a + a * a + (a * a + a * a)
Module: Mathlib.Algebra.Ring.BooleanRing

Goal state before:
pp: α : Type u_1
inst✝ : BooleanRing α
a b : α
⊢ (a + b) * (a + b) = a * a + a * b + (b * a + b * b)

Tactic:
add_mul,

Goal state after:
α : Type u_1
inst✝ : BooleanRing α
a b : α
⊢ a * (a + b) + b * (a + b) = a * a + a * b + (b * a + b * b)
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 : Mon Cᵒᵖ
⊢ μ.unop ≫ unop A.X ◁ μ.unop = μ.unop ≫ μ.unop ▷ unop A.X ≫ (α_ (unop A.X) (unop A.X) (unop A.X)).hom

Tactic:
by
    rw [← unop_whiskerRight, ← unop_whiskerLeft, ← unop_comp_assoc, ← unop_comp,
      MonObj.mul_assoc_flip]
    rfl

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
P : Type u_3
inst✝⁶ : CommSemiring P
Q : Type u_4
inst✝⁵ : CommSemiring Q
inst✝⁴ : Algebra P Q
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R →+* P
r : R
inst✝¹ : Away r S
inst✝ : Away (f r) Q
⊢ Function.Injective ⇑(map S Q f r) ↔ ∀ (a : R), f a = 0 → ∃ n, r ^ n * a = 0

Tactic:
rw [injective_iff_map_eq_zero]

Goal state after:
R : Type u_1
inst✝⁷ : CommSemiring R
P : Type u_3
inst✝⁶ : CommSemiring P
Q : Type u_4
inst✝⁵ : CommSemiring Q
inst✝⁴ : Algebra P Q
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R →+* P
r : R
inst✝¹ : Away r S
inst✝ : Away (f r) Q
⊢ (∀ (a : S), (map S Q f r) a = 0 → a = 0) ↔ ∀ (a : R), f a = 0 → ∃ n, r ^ n * a = 0
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
x✝ : R
h : x✝ ∈ { ringCon := sInf {s_1 | ∀ (x y : R), x - y ∈ s → s_1 x y} }
I : TwoSidedIdeal R
hI : s ⊆ ↑I
x y : R
⊢ x - y ∈ s → I.ringCon x y

Tactic:
hxy

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
x✝ : R
h : x✝ ∈ { ringCon := sInf {s_1 | ∀ (x y : R), x - y ∈ s → s_1 x y} }
I : TwoSidedIdeal R
hI : s ⊆ ↑I
x y : R
hxy : x - y ∈ s
⊢ I.ringCon x y
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case refine_2
S : Type u_4
T : Type u_5
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra S T
R : Type u_6
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
h₁ : Function.Surjective ⇑(algebraMap S T)
h₂ : Function.Surjective ⇑(algebraMap R S)
r : R
hr : IsUnit ((algebraMap R T) r)
n : ℕ
hn : r ^ n • RingHom.ker (algebraMap R T) ≤ RingHom.ker (algebraMap R S)
⊢ Ideal.map (algebraMap R S) (r ^ n • Ideal.comap (algebraMap R S) (RingHom.ker (algebraMap S T))) ≤ ⊥

Tactic:
RingHom.comap_ker,

Goal state after:
case refine_2
S : Type u_4
T : Type u_5
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra S T
R : Type u_6
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
h₁ : Function.Surjective ⇑(algebraMap S T)
h₂ : Function.Surjective ⇑(algebraMap R S)
r : R
hr : IsUnit ((algebraMap R T) r)
n : ℕ
hn : r ^ n • RingHom.ker (algebraMap R T) ≤ RingHom.ker (algebraMap R S)
⊢ Ideal.map (algebraMap R S) (r ^ n • RingHom.ker ((algebraMap S T).comp (algebraMap R S))) ≤ ⊥
Module: Mathlib.RingTheory.LocalRing.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : Ring S
inst✝ : Nontrivial S
f : R →+* S
hf : Function.Surjective ⇑f
a : R
⊢ IsUnit (1 - a) → IsUnit (1 - f a)

Tactic:
← f.map_one,

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : Ring S
inst✝ : Nontrivial S
f : R →+* S
hf : Function.Surjective ⇑f
a : R
⊢ IsUnit (1 - a) → IsUnit (f 1 - f a)
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x : R
hx : x ∈ ⊥.jacobson
y z : R
hz : z * y * x + z - 1 ∈ ⊥
⊢ (x * y + 1) * z = 1

Tactic:
add_mul,

Goal state after:
R : Type u
inst✝ : CommRing R
x : R
hx : x ∈ ⊥.jacobson
y z : R
hz : z * y * x + z - 1 ∈ ⊥
⊢ x * y * z + 1 * z = 1
Module: Mathlib.RingTheory.Localization.Away.Basic

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

Tactic:
IsLocalization.mk'_eq_iff_eq

Goal state after:
case neg
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 : ℕ
h : n < m
⊢ (algebraMap R B) (↑(Submonoid.pow x m) * 1) = (algebraMap R B) (↑(Submonoid.pow x (m - n)) * x ^ n)
Module: Mathlib.Algebra.Module.LocalizedModule.IsLocalization

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring Aₛ
inst✝² : Algebra A Aₛ
inst✝¹ : Algebra R Aₛ
inst✝ : IsScalarTower R A Aₛ
⊢ (∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R Aₛ)) ↑x)) ↔
    ∀ (y : ↥(Algebra.algebraMapSubmonoid A S)), IsUnit ((algebraMap A Aₛ) ↑y)

pp: case refine_2
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring Aₛ
inst✝² : Algebra A Aₛ
inst✝¹ : Algebra R Aₛ
inst✝ : IsScalarTower R A Aₛ
x✝ : Aₛ
⊢ (∃ x, x.2 • x✝ = (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x.1) ↔
    ∃ x, x✝ * (algebraMap A Aₛ) ↑x.2 = (algebraMap A Aₛ) x.1

pp: case refine_3
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring Aₛ
inst✝² : Algebra A Aₛ
inst✝¹ : Algebra R Aₛ
inst✝ : IsScalarTower R A Aₛ
x✝¹ x✝ : A
⊢ ((IsScalarTower.toAlgHom R A Aₛ).toLinearMap x✝¹ = (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x✝ →
      ∃ c, c • x✝¹ = c • x✝) ↔
    (algebraMap A Aₛ) x✝¹ = (algebraMap A Aₛ) x✝ → ∃ c, ↑c * x✝¹ = ↑c * x✝

Tactic:
· simp_rw [← (Algebra.lmul R Aₛ).commutes, Algebra.lmul_isUnit_iff, Subtype.forall,
      Algebra.algebraMapSubmonoid, ← SetLike.mem_coe, Submonoid.coe_map,
      Set.forall_mem_image, ← IsScalarTower.algebraMap_apply]

Goal state after:
case refine_2
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring Aₛ
inst✝² : Algebra A Aₛ
inst✝¹ : Algebra R Aₛ
inst✝ : IsScalarTower R A Aₛ
x✝ : Aₛ
⊢ (∃ x, x.2 • x✝ = (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x.1) ↔
    ∃ x, x✝ * (algebraMap A Aₛ) ↑x.2 = (algebraMap A Aₛ) x.1

case refine_3
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring Aₛ
inst✝² : Algebra A Aₛ
inst✝¹ : Algebra R Aₛ
inst✝ : IsScalarTower R A Aₛ
x✝¹ x✝ : A
⊢ ((IsScalarTower.toAlgHom R A Aₛ).toLinearMap x✝¹ = (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x✝ →
      ∃ c, c • x✝¹ = c • x✝) ↔
    (algebraMap A Aₛ) x✝¹ = (algebraMap A Aₛ) x✝ → ∃ c, ↑c * x✝¹ = ↑c * x✝
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: case mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : C
h₂ : MonObj X
one✝ : 𝟙_ C ⟶ X
mul✝ : X ⊗ X ⟶ X
one_mul✝ : one✝ ▷ X ≫ mul✝ = (λ_ X).hom
mul_one✝ : X ◁ one✝ ≫ mul✝ = (ρ_ X).hom
mul_assoc✝ : mul✝ ▷ X ≫ mul✝ = (α_ X X X).hom ≫ X ◁ mul✝ ≫ mul✝
H : μ = μ
this : η = η
⊢ { one := one✝, mul := mul✝, one_mul := one_mul✝, mul_one := mul_one✝, mul_assoc := mul_assoc✝ } = h₂

Tactic:
cases h₂

Goal state after:
case mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : C
one✝¹ : 𝟙_ C ⟶ X
mul✝¹ : X ⊗ X ⟶ X
one_mul✝¹ : one✝¹ ▷ X ≫ mul✝¹ = (λ_ X).hom
mul_one✝¹ : X ◁ one✝¹ ≫ mul✝¹ = (ρ_ X).hom
mul_assoc✝¹ : mul✝¹ ▷ X ≫ mul✝¹ = (α_ X X X).hom ≫ X ◁ mul✝¹ ≫ mul✝¹
one✝ : 𝟙_ C ⟶ X
mul✝ : X ⊗ X ⟶ X
one_mul✝ : one✝ ▷ X ≫ mul✝ = (λ_ X).hom
mul_one✝ : X ◁ one✝ ≫ mul✝ = (ρ_ X).hom
mul_assoc✝ : mul✝ ▷ X ≫ mul✝ = (α_ X X X).hom ≫ X ◁ mul✝ ≫ mul✝
H : μ = μ
this : η = η
⊢ { one := one✝¹, mul := mul✝¹, one_mul := one_mul✝¹, mul_one := mul_one✝¹, mul_assoc := mul_assoc✝¹ } =
    { one := one✝, mul := mul✝, one_mul := one_mul✝, mul_one := mul_one✝, mul_assoc := mul_assoc✝ }
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝¹³ : Category.{v₁, u₁} C
inst✝¹² : MonoidalCategory C
M✝ N✝ O X : C
inst✝¹¹ : MonObj M✝
inst✝¹⁰ : MonObj N✝
inst✝⁹ : MonObj O
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : MonoidalCategory D
E : Type u₃
inst✝⁶ : Category.{v₃, u₃} E
inst✝⁵ : MonoidalCategory E
F F' : C ⥤ D
G : D ⥤ E
inst✝⁴ : BraidedCategory C
inst✝³ : BraidedCategory D
inst✝² : F.LaxBraided
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
⊢ η ≫ «μ» F M N = η

Tactic:
simp [← Functor.map_comp, leftUnitor_inv_comp_tensorHom_assoc]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit (t₂.pasteHoriz t₁ hi₂)
⊢ IsLimit t₁

Tactic:
by
  apply PullbackCone.isLimitAux'
  intro s
  -- Obtain the induced morphism from the universal property of the big square
  obtain ⟨l, hl, hl'⟩ := PullbackCone.IsLimit.lift' H' s.fst (s.snd ≫ f₂)
    (by rw [Category.assoc, ← t₂.condition, reassoc_of% s.condition, ← hi₂])
  refine ⟨l, hl, ?_, ?_⟩
  -- To check that `l` is compatible with the projections, we use the universal property of `t₂`
  · apply PullbackCone.IsLimit.hom_ext H
    · simp [← s.condition, ← hl, ← t₁.condition, ← hi₂]
    · simpa using hl'
  -- Uniqueness of the lift follows from the universal property of the big square
  · intro m hm₁ hm₂
    apply PullbackCone.IsLimit.hom_ext H'
    · simpa [hm₁] using hl.symm
    · simpa [← hm₂] using hl'.symm

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

Goal state before:
pp: case pos
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
e : Localization S ⊗[R] M ≃ₗ[R] M' :=
  LinearEquiv.restrictScalars R (LocalizedModule.equivTensorProduct S M).symm ≪≫ₗ IsLocalizedModule.iso S f
e' : Localization S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ M' :=
  finsuppRight R R (Localization S) M α ≪≫ₗ Finsupp.mapRange.linearEquiv e
a : α
m : M
b : α
h : a = b
⊢ f m = e (1 ⊗ₜ[R] m)

Tactic:
simp [e]

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_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
⊢ lift S g h ∘ₗ mkLinearMap S M = g

Tactic:
ext x
  simp [LocalizedModule.lift_mk]

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
m : M'
inj : Function.Injective fun r ↦ r • m
s : ↥S
r r' : R
eq : (fun x ↦ ↑s * x) r = (fun x ↦ ↑s * x) r'
⊢ r = r'

Tactic:
by
    have := congr_arg (· • m) eq
    simp_rw [mul_smul, ← Submonoid.smul_def, smul_inj f] at this
    exact inj this

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
m : M
s : ↥S
⊢ (fromLocalizedModule S f) (LocalizedModule.mk (s • m) s) = f m

Tactic:
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.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᴸ C
F' : F.PseudoCore
a✝ b✝ c✝ : B
f : a✝ ⟶ b✝
g h : b✝ ⟶ c✝
η : g ⟶ h
⊢ F.map₂ (f ◁ η) = (F'.mapCompIso f g).hom ≫ (F'.mapCompIso f g).inv ≫ F.map₂ (f ◁ η)

Tactic:
hom_inv_id_assoc

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᴸ C
F' : F.PseudoCore
a✝ b✝ c✝ : B
f : a✝ ⟶ b✝
g h : b✝ ⟶ c✝
η : g ⟶ h
⊢ F.map₂ (f ◁ η) = F.map₂ (f ◁ η)
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᴸ C
F' : F.PseudoCore
a✝ b✝ c✝ : B
f✝ g✝ : a✝ ⟶ b✝
η : f✝ ⟶ g✝
h : b✝ ⟶ c✝
⊢ F.map₂ (η ▷ h) = (F'.mapCompIso f✝ h).hom ≫ (F'.mapCompIso f✝ h).inv ≫ F.map₂ (η ▷ h)

Tactic:
hom_inv_id_assoc

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᴸ C
F' : F.PseudoCore
a✝ b✝ c✝ : B
f✝ g✝ : a✝ ⟶ b✝
η : f✝ ⟶ g✝
h : b✝ ⟶ c✝
⊢ F.map₂ (η ▷ h) = F.map₂ (η ▷ h)
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.EssentiallySmall.{w, v, u} P
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
left✝ : Q ≤ P
right✝ : P ≤ Q.isoClosure
⊢ ∃ Q, ∃ (_ : ObjectProperty.Small.{w, v, u} Q), P.isoClosure ≤ Q.isoClosure

Tactic:
exact ⟨Q, inferInstance, by rwa [isoClosure_le_iff]⟩

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case intro.refine_2
R : Type w₁
A : Type w₂
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FinitePresentation R A
ι : Type v
inst✝ : Finite ι
ι' : Type v
w✝ : Fintype ι'
f : MvPolynomial ι' R →ₐ[R] A
hf_surj : Surjective ⇑f
hf_ker : (RingHom.ker f.toRingHom).FG
g : MvPolynomial (ι ⊕ ι') R →ₐ[R] MvPolynomial ι A := (MvPolynomial.mapAlgHom f).comp ↑(MvPolynomial.sumAlgEquiv R ι ι')
val✝ : Fintype (ι ⊕ ι')
⊢ (RingHom.ker (MvPolynomial.mapAlgHom f).toRingHom).FG

Tactic:
rw [AlgHom.toRingHom_eq_coe, MvPolynomial.mapAlgHom_coe_ringHom, MvPolynomial.ker_map]

Goal state after:
case intro.refine_2
R : Type w₁
A : Type w₂
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FinitePresentation R A
ι : Type v
inst✝ : Finite ι
ι' : Type v
w✝ : Fintype ι'
f : MvPolynomial ι' R →ₐ[R] A
hf_surj : Surjective ⇑f
hf_ker : (RingHom.ker f.toRingHom).FG
g : MvPolynomial (ι ⊕ ι') R →ₐ[R] MvPolynomial ι A := (MvPolynomial.mapAlgHom f).comp ↑(MvPolynomial.sumAlgEquiv R ι ι')
val✝ : Fintype (ι ⊕ ι')
⊢ (Ideal.map MvPolynomial.C (RingHom.ker ↑f)).FG
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case refine_1.inl
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✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ⇑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker f.toRingHom
RX : Type (max w₁ 0) := MvPolynomial (Fin n) R
AX : Type (max w₂ 0) := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : ↥t → MvPolynomial (Fin n) R
ht' : ∀ (i : ↥t), f (t' i) = (algebraMap A B) ↑i
ht'' : adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : ↥t → AX := fun x ↦ MvPolynomial.C ↑x - (MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
leI :
  Ideal.span (⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
x✝ : MvPolynomial (Fin n) A
hx✝ : (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X)) x✝ = 0
s₀ : Set (MvPolynomial (Fin n) A) := ⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x✝ ∈ adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
x : A
hx : x ∈ ↑t
⊢ (algebraMap A AX) x ∈ (MvPolynomial.map (algebraMap R A)).range.toAddSubmonoid ⊔ (Ideal.span s₀).toAddSubmonoid

Tactic:
MvPolynomial.algebraMap_eq,

Goal state after:
case refine_1.inl
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✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ⇑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker f.toRingHom
RX : Type (max w₁ 0) := MvPolynomial (Fin n) R
AX : Type (max w₂ 0) := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : ↥t → MvPolynomial (Fin n) R
ht' : ∀ (i : ↥t), f (t' i) = (algebraMap A B) ↑i
ht'' : adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : ↥t → AX := fun x ↦ MvPolynomial.C ↑x - (MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
leI :
  Ideal.span (⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
x✝ : MvPolynomial (Fin n) A
hx✝ : (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X)) x✝ = 0
s₀ : Set (MvPolynomial (Fin n) A) := ⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x✝ ∈ adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
x : A
hx : x ∈ ↑t
⊢ MvPolynomial.C x ∈ (MvPolynomial.map (algebraMap R A)).range.toAddSubmonoid ⊔ (Ideal.span s₀).toAddSubmonoid
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: case mk
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
g : X.Hom Y
base✝ : X.base ⟶ Y.base
fiber✝ : (F.map base✝).toFunctor.obj X.fiber ⟶ Y.fiber
w_base : { base := base✝, fiber := fiber✝ }.base = g.base
w_fiber : eqToHom ⋯ ≫ { base := base✝, fiber := fiber✝ }.fiber = g.fiber
⊢ { base := base✝, fiber := fiber✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
base✝¹ : X.base ⟶ Y.base
fiber✝¹ : (F.map base✝¹).toFunctor.obj X.fiber ⟶ Y.fiber
base✝ : X.base ⟶ Y.base
fiber✝ : (F.map base✝).toFunctor.obj X.fiber ⟶ Y.fiber
w_base : { base := base✝¹, fiber := fiber✝¹ }.base = { base := base✝, fiber := fiber✝ }.base
w_fiber : eqToHom ⋯ ≫ { base := base✝¹, fiber := fiber✝¹ }.fiber = { base := base✝, fiber := fiber✝ }.fiber
⊢ { base := base✝¹, fiber := fiber✝¹ } = { base := base✝, fiber := fiber✝ }
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: 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
c : Cocone (F ⋙ G)
X : D
Y : C
f : X ⟶ F.obj Y
⊢ (extendCocone.obj c).ι.app X = G.map f ≫ c.ι.app Y

Tactic:
by
  apply induction (k₀ := f) (z := rfl) F fun Z g =>
    G.map g ≫ c.ι.app Z = G.map f ≫ c.ι.app Y
  · intro _ _ _ _ _ h₁ h₂
    simp [← h₁, ← Functor.comp_map, c.ι.naturality, h₂]
  · intro _ _ _ _ _ h₁ h₂
    simp [← h₂, ← h₁, ← Functor.comp_map, c.ι.naturality]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y B X : C
f : X ⟶ B
inst✝ : EffectiveEpi f
c : PullbackCone f f
hc : IsLimit c
s : Cocone (parallelPair c.fst c.snd)
⊢ ∀ (j : WalkingParallelPair),
    (Cofork.ofπ f ⋯).ι.app j ≫ EffectiveEpi.desc f (s.ι.app WalkingParallelPair.one) ⋯ = s.ι.app j

Tactic:
have := EffectiveEpi.fac f (s.ι.app WalkingParallelPair.one) fun g₁ g₂ hg ↦ (by
      simp only [Cofork.app_one_eq_π]
      rw [← PullbackCone.IsLimit.lift_snd hc g₁ g₂ hg,
        Category.assoc, ← Cofork.app_zero_eq_comp_π_right]
      simp)

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y B X : C
f : X ⟶ B
inst✝ : EffectiveEpi f
c : PullbackCone f f
hc : IsLimit c
s : Cocone (parallelPair c.fst c.snd)
this : f ≫ EffectiveEpi.desc f (s.ι.app WalkingParallelPair.one) ⋯ = s.ι.app WalkingParallelPair.one
⊢ ∀ (j : WalkingParallelPair),
    (Cofork.ofπ f ⋯).ι.app j ≫ EffectiveEpi.desc f (s.ι.app WalkingParallelPair.one) ⋯ = s.ι.app j