mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case h2
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Semiring R
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
r : R
x : tsze R M
h : r * x.fst = 1
⊢ r •> x.snd + (0 + -(r •> x.snd <• r)) <• x.fst = 0

Tactic:
zero_add,

Goal state after:
case h2
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Semiring R
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
r : R
x : tsze R M
h : r * x.fst = 1
⊢ r •> x.snd + -(r •> x.snd <• r) <• x.fst = 0
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case h2
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Semiring R
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
x : tsze R M
r : R
h : x.fst * r = 1
⊢ x.fst •> (0 + -(r •> (x.snd <• r))) + x.snd <• r = 0

Tactic:
zero_add,

Goal state after:
case h2
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Semiring R
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
x : tsze R M
r : R
h : x.fst * r = 1
⊢ x.fst •> -(r •> (x.snd <• r)) + x.snd <• r = 0
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R' : Type u
M : Type v
inst✝¹² : CommSemiring R'
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R' M
inst✝⁹ : Module R'ᵐᵒᵖ M
inst✝⁸ : IsCentralScalar R' M
N : Type u_3
P : Type u_4
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R' N
inst✝⁵ : Module R'ᵐᵒᵖ N
inst✝⁴ : IsCentralScalar R' N
inst✝³ : AddCommMonoid P
inst✝² : Module R' P
inst✝¹ : Module R'ᵐᵒᵖ P
inst✝ : IsCentralScalar R' P
f : M →ₗ[R'] N
g : N →ₗ[R'] P
⊢ map (g ∘ₗ f) = (map g).comp (map f)

Tactic:
apply algHom_ext
  simp only [map_inr, LinearMap.coe_comp, Function.comp_apply, AlgHom.coe_comp, forall_const]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: case refine_1
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
z : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑X
⊢ ↑((restrictScalars f).obj (of S S)) →ₗ[R] ↑X →ₗ[R] ↑Y

Tactic:
refine
    { toFun s := HomEquiv.evalAt f s g, map_add' := fun (s₁ s₂ : S) ↦ ?_,
      map_smul' := fun (r : R) (s : S) ↦ ?_ }

Goal state after:
case refine_1.refine_1
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
z : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑X
s₁ s₂ : S
⊢ evalAt f (s₁ + s₂) g = evalAt f s₁ g + evalAt f s₂ g

case refine_1.refine_2
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
z : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑X
r : R
s : S
⊢ evalAt f (r • s) g = (RingHom.id R) r • evalAt f s g
Module: Mathlib.Algebra.Ring.BooleanRing

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a : α
⊢ 0 + a + 0 = a

Tactic:
zero_add,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a : α
⊢ a + 0 = a
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a b : R
n : ℕ
ha : Irreducible a
hb : b ≠ 0
⊢ ↑n ≤ emultiplicity a b ↔ replicate n (normalize a) ≤ normalizedFactors b

Tactic:
rw [← pow_dvd_iff_le_emultiplicity]
  revert b
  induction n with
  | zero => simp
  | succ n ih => ?_
  intro b hb
  constructor
  · rintro ⟨c, rfl⟩
    rw [Ne, pow_succ', mul_assoc, mul_eq_zero, not_or] at hb
    rw [pow_succ', mul_assoc, normalizedFactors_mul hb.1 hb.2, replicate_succ,
      normalizedFactors_irreducible ha, singleton_add, cons_le_cons_iff, ← ih hb.2]
    apply Dvd.intro _ rfl
  · rw [Multiset.le_iff_exists_add]
    rintro ⟨u, hu⟩
    rw [← (prod_normalizedFactors hb).dvd_iff_dvd_right, hu, prod_add, prod_replicate]
    exact (Associated.pow_pow <| associated_normalize a).dvd.trans (Dvd.intro u.prod rfl)

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: case a
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
a b : R
ha : Irreducible a
hb : b ≠ 0
⊢ emultiplicity a b < ↑(count (normalize a) (normalizedFactors b)) + 1

Tactic:
rw [← Nat.cast_one, ← Nat.cast_add, lt_iff_not_ge,
      le_emultiplicity_iff_replicate_le_normalizedFactors ha hb, ← le_count_iff_replicate_le]

Goal state after:
case a
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
a b : R
ha : Irreducible a
hb : b ≠ 0
⊢ ¬count (normalize a) (normalizedFactors b) + 1 ≤ count (normalize a) (normalizedFactors b)
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case refine_3
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
x y : R
inst✝¹ : Away x S
inst✝ : Away ((algebraMap R S) y) T
a b : R
h : (algebraMap S T) ((algebraMap R S) a) = (algebraMap S T) ((algebraMap R S) b)
n : ℕ
hn : (algebraMap R S) (y ^ n * a) = (algebraMap R S) (y ^ n * b)
⊢ ∃ n, (y * x) ^ n * a = (y * x) ^ n * b

Tactic:
obtain ⟨m, hm⟩ := exists_of_eq x hn

Goal state after:
case refine_3
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
x y : R
inst✝¹ : Away x S
inst✝ : Away ((algebraMap R S) y) T
a b : R
h : (algebraMap S T) ((algebraMap R S) a) = (algebraMap S T) ((algebraMap R S) b)
n : ℕ
hn : (algebraMap R S) (y ^ n * a) = (algebraMap R S) (y ^ n * b)
m : ℕ
hm : x ^ m * (y ^ n * a) = x ^ m * (y ^ n * b)
⊢ ∃ n, (y * x) ^ n * a = (y * x) ^ n * b
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: S : Type u_2
inst✝¹ : CommSemiring S
R : Type u_4
inst✝ : CommRing R
f : R →+* S
a b : R
h : a ∣ b
H : ∀ (a_1 : R), f a_1 = 0 → ∃ n, a ^ n * a_1 = 0
⊢ ∀ (a : R), f a = 0 → ∃ n, b ^ n * a = 0

Tactic:
obtain ⟨b, rfl⟩ := h

Goal state after:
S : Type u_2
inst✝¹ : CommSemiring S
R : Type u_4
inst✝ : CommRing R
f : R →+* S
a : R
H : ∀ (a_1 : R), f a_1 = 0 → ∃ n, a ^ n * a_1 = 0
b : R
⊢ ∀ (a_1 : R), f a_1 = 0 → ∃ n, (a * b) ^ n * a_1 = 0
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
f : R →+* S
a b : R
h : a ∣ b
H : ∀ (a_1 : S), ∃ b m, f b = f a ^ m * a_1
⊢ ∀ (a : S), ∃ b_1 m, f b_1 = f b ^ m * a

Tactic:
obtain ⟨b, rfl⟩ := h

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
f : R →+* S
a : R
H : ∀ (a_1 : S), ∃ b m, f b = f a ^ m * a_1
b : R
⊢ ∀ (a_1 : S), ∃ b_1 m, f b_1 = f (a * b) ^ m * a_1
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
f : R →+* S
a b : R
H : Function.Surjective ⇑(awayMap f (a * b))
⊢ Function.Surjective ⇑(awayMap (awayMap f a) ((algebraMap R (Away a)) b))

Tactic:
rw [awayMap_surjective_iff] at H ⊢
  suffices ∀ (s : S) (n : ℕ), ∃ c l m k, f (a ^ (k + n) * c) =
      f (a ^ (k + l) * b ^ m) * s by
    simpa [Function.Surjective, (IsLocalization.mk'_surjective (.powers (f a))).forall, ← map_pow,
      (IsLocalization.mk'_surjective (.powers a)).exists, Submonoid.mem_powers_iff, pow_add,
      Localization.awayMap, IsLocalization.Away.map, IsLocalization.map_mk', ← mul_assoc,
      IsLocalization.mk'_eq_iff_eq, ← map_mul, IsLocalization.eq_iff_exists (.powers (f a)),
      IsLocalization.mul_mk'_eq_mk'_of_mul]
  intro s n
  obtain ⟨c, m, e⟩ := H s
  exact ⟨c, n + m, m, 0, by simp [e, pow_add]; ring⟩

Goal state after:
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:
rwa [add_mul, one_mul, ← sub_eq_zero, mul_right_comm, mul_comm _ z, mul_right_comm]

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

Goal state before:
pp: case inl.inr
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 : ℤ
hn : 0 ≤ n
hm : m < 0
this : n + m = ↑n.natAbs - ↑m.natAbs
⊢ mk' B (x ^ n.natAbs) (Submonoid.pow x m.natAbs) = (algebraMap R B) x ^ n.natAbs * mk' B 1 (Submonoid.pow x m.natAbs)

Tactic:
IsLocalization.mk'_eq_mul_mk'_one,

Goal state after:
case inl.inr
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 : ℤ
hn : 0 ≤ n
hm : m < 0
this : n + m = ↑n.natAbs - ↑m.natAbs
⊢ (algebraMap R B) (x ^ n.natAbs) * mk' B 1 (Submonoid.pow x m.natAbs) =
    (algebraMap R B) x ^ n.natAbs * mk' B 1 (Submonoid.pow x m.natAbs)
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case inr.inl
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 : ℤ
hn : n < 0
hm : 0 ≤ m
this : n + m = ↑m.natAbs - ↑n.natAbs
⊢ mk' B (x ^ m.natAbs) (Submonoid.pow x n.natAbs) = mk' B 1 (Submonoid.pow x n.natAbs) * (algebraMap R B) x ^ m.natAbs

Tactic:
IsLocalization.mk'_eq_mul_mk'_one,

Goal state after:
case inr.inl
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 : ℤ
hn : n < 0
hm : 0 ≤ m
this : n + m = ↑m.natAbs - ↑n.natAbs
⊢ (algebraMap R B) (x ^ m.natAbs) * mk' B 1 (Submonoid.pow x n.natAbs) =
    mk' B 1 (Submonoid.pow x n.natAbs) * (algebraMap R B) x ^ m.natAbs
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
M : C
inst✝ : MonObj M
⊢ (tensorμ (𝟙_ C) M (𝟙_ C) M ≫ ((λ_ (𝟙_ C)).hom ⊗ₘ μ)) ≫ (λ_ M).hom = ((λ_ M).hom ⊗ₘ (λ_ M).hom) ≫ μ

Tactic:
by
  rw [← Category.comp_id (λ_ (𝟙_ C)).hom, ← Category.id_comp μ, ← tensorHom_comp_tensorHom]
  simp only [tensorHom_id, id_tensorHom]
  slice_lhs 3 4 => rw [leftUnitor_naturality]
  slice_lhs 1 3 => rw [← leftUnitor_monoidal]
  simp only [Category.id_comp]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : SymmetricCategory C
X Y : C
inst✝¹ : MonObj X
inst✝ : MonObj Y
⊢ (β_ X Y).hom ▷ (X ⊗ Y) ≫
      ((((((𝟙 ((Y ⊗ X) ⊗ X ⊗ Y) ≫ (α_ Y X (X ⊗ Y)).hom) ≫ Y ◁ X ◁ (β_ X Y).hom) ≫ Y ◁ (α_ X Y X).inv) ≫
              Y ◁ (β_ X Y).hom ▷ X) ≫
            Y ◁ (α_ Y X X).hom) ≫
          (α_ Y Y (X ⊗ X)).inv) ≫
        (μ ⊗ₘ μ) =
    ((β_ X Y).hom ⊗ₘ (β_ X Y).hom) ≫
      (α_ Y X (Y ⊗ X)).hom ≫
        Y ◁ (α_ X Y X).inv ≫ Y ◁ (β_ X Y).hom ▷ X ≫ Y ◁ (α_ Y X X).hom ≫ (α_ Y Y (X ⊗ X)).inv ≫ (μ ⊗ₘ μ)

Tactic:
rw [Category.id_comp]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : SymmetricCategory C
X Y : C
inst✝¹ : MonObj X
inst✝ : MonObj Y
⊢ (β_ X Y).hom ▷ (X ⊗ Y) ≫
      ((((((α_ Y X (X ⊗ Y)).hom ≫ Y ◁ X ◁ (β_ X Y).hom) ≫ Y ◁ (α_ X Y X).inv) ≫ Y ◁ (β_ X Y).hom ▷ X) ≫
            Y ◁ (α_ Y X X).hom) ≫
          (α_ Y Y (X ⊗ X)).inv) ≫
        (μ ⊗ₘ μ) =
    ((β_ X Y).hom ⊗ₘ (β_ X Y).hom) ≫
      (α_ Y X (Y ⊗ X)).hom ≫
        Y ◁ (α_ X Y X).inv ≫ Y ◁ (β_ X Y).hom ▷ X ≫ Y ◁ (α_ Y X X).hom ≫ (α_ Y Y (X ⊗ X)).inv ≫ (μ ⊗ₘ μ)
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₁
s : PullbackCone (g₁ ≫ g₂) i₃
l₂ : s.pt ⟶ t₂.pt
hl₂ : l₂ ≫ t₂.fst = s.fst ≫ g₁
hl₂' : l₂ ≫ t₂.snd = s.snd
l₁ : s.pt ⟶ t₁.pt
hl₁ : l₁ ≫ t₁.fst = s.fst
hl₁' : l₁ ≫ t₁.snd = l₂
⊢ l₁ ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd

Tactic:
simp [reassoc_of% hl₁', hl₂']

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₁
s : PullbackCone (g₁ ≫ g₂) i₃
l₂ : s.pt ⟶ t₂.pt
hl₂ : l₂ ≫ t₂.fst = s.fst ≫ g₁
hl₂' : l₂ ≫ t₂.snd = s.snd
l₁ : s.pt ⟶ t₁.pt
hl₁ : l₁ ≫ t₁.fst = s.fst
hl₁' : l₁ ≫ t₁.snd = l₂
m : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hm₁ : m ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst
hm₂ : m ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd
⊢ m = l₁

Tactic:
apply PullbackCone.IsLimit.hom_ext H' (by simpa [hl₁] using hm₁)

Goal state after:
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₁
s : PullbackCone (g₁ ≫ g₂) i₃
l₂ : s.pt ⟶ t₂.pt
hl₂ : l₂ ≫ t₂.fst = s.fst ≫ g₁
hl₂' : l₂ ≫ t₂.snd = s.snd
l₁ : s.pt ⟶ t₁.pt
hl₁ : l₁ ≫ t₁.fst = s.fst
hl₁' : l₁ ≫ t₁.snd = l₂
m : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hm₁ : m ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst
hm₂ : m ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd
⊢ m ≫ t₁.snd = l₁ ≫ t₁.snd
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
s : ↥S
p : LocalizedModule S M
m : M
t : ↥S
⊢ ((algebraMap R (End R (LocalizedModule S M))) ↑s) ((divBy s) (mk m t)) = mk m t

Tactic:
by
    rw [divBy_apply, Module.algebraMap_end_apply, LocalizedModule.liftOn_mk, smul'_mk,
      ← Submonoid.smul_def, mk_cancel_common_right _ s]

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Products

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : HasBinaryCoproducts C
A : (coprodMonad X).Algebra
⊢ coprod.inr ≫
      (coprodMonad X).map (Iso.refl ((𝟭 (coprodMonad X).Algebra).obj A).A).hom ≫
        ((algebraToUnder X ⋙ underToAlgebra X).obj A).a =
    coprod.inr ≫ ((𝟭 (coprodMonad X).Algebra).obj A).a ≫ (Iso.refl ((𝟭 (coprodMonad X).Algebra).obj A).A).hom

Tactic:
by simpa using A.unit.symm

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

Goal state before:
pp: R S : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
R' S' : Type u
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing S'
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R' S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
h : IsPushout (ofHom (algebraMap R R')) (ofHom (algebraMap R S)) (ofHom (algebraMap R' S')) (ofHom (algebraMap S S'))
e : R' ⊗[R] S ≃+* S' := (⋯.isoPushout ≪≫ h.isoPushout.symm).commRingCatIsoToRingEquiv
h2 :
  ∀ (r : R'),
    (ConcreteCategory.hom ⋯.isoPushout.hom) (r ⊗ₜ[R] 1) =
      (ConcreteCategory.hom (pushout.inl (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))) r
h3 :
  ∀ (x : R'),
    (Hom.hom h.isoPushout.inv) ((Hom.hom (pushout.inl (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))) x) =
      (algebraMap R' S') x
e' : R' ⊗[R] S ≃ₐ[R'] S' :=
  let __spread.0 := e;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
s : S
h1 :
  (ConcreteCategory.hom ⋯.isoPushout.hom) ((algebraMap S (R' ⊗[R] S)) s) =
    (ConcreteCategory.hom (pushout.inr (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))) s
h4 :
  ∀ (x : S),
    (Hom.hom h.isoPushout.inv) ((Hom.hom (pushout.inr (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))) x) =
      (algebraMap S S') x
⊢ (e'.toRingEquiv.toRingHom.comp (algebraMap S (R' ⊗[R] S))) s = (algebraMap S S') s

Tactic:
simp [Iso.commRingCatIsoToRingEquiv, h1, e', e, h4]

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''
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 : M →ₗ[R] M''
inst✝⁶ : IsLocalizedModule S f
M₁ : Type u_6
M₂ : Type u_7
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
S₁ S₂ : Submonoid R
h : S₁ ≤ S₂
f₁ : M →ₗ[R] M₁
f₂ : M →ₗ[R] M₂
inst✝¹ : IsLocalizedModule S₁ f₁
inst✝ : IsLocalizedModule S₂ f₂
⊢ ∀ {x₁ x₂ : M₁}, (liftOfLE S₁ S₂ h f₁ f₂) x₁ = (liftOfLE S₁ S₂ h f₁ f₂) x₂ → ∃ c, c • x₁ = c • x₂

Tactic:
intro x₁ x₂ e

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''
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 : M →ₗ[R] M''
inst✝⁶ : IsLocalizedModule S f
M₁ : Type u_6
M₂ : Type u_7
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
S₁ S₂ : Submonoid R
h : S₁ ≤ S₂
f₁ : M →ₗ[R] M₁
f₂ : M →ₗ[R] M₂
inst✝¹ : IsLocalizedModule S₁ f₁
inst✝ : IsLocalizedModule S₂ f₂
x₁ x₂ : M₁
e : (liftOfLE S₁ S₂ h f₁ f₂) x₁ = (liftOfLE S₁ S₂ h f₁ f₂) x₂
⊢ ∃ c, c • x₁ = c • x₂
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
F : J ⥤ Arrow T
i₁ : HasLimit (F ⋙ leftFunc)
i₂ : HasLimit (F ⋙ rightFunc)
⊢ HasLimit F

Tactic:
have : HasLimit (F ⋙ Comma.fst _ _) := i₁
  have : HasLimit (F ⋙ Comma.snd _ _) := i₂
  apply Comma.hasLimit

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
X : T
G : A ⥤ T
F : J✝ ⥤ StructuredArrow X G
inst✝¹ : HasLimitsOfSize.{w, w', v₁, u₁} A
inst✝ : PreservesLimitsOfSize.{w, w', v₁, v₃, u₁, u₃} G
J : Type w'
hJ : Category.{w, w'} J
⊢ HasLimitsOfShape J (StructuredArrow X G)

Tactic:
by infer_instance

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

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R M
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N : Type u_6
N' : Type u_7
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid N'
inst✝² : Module R N
inst✝¹ : Module R N'
g : N →ₗ[R] N'
inst✝ : IsLocalizedModule S g
h : M →ₗ[R] N
h_inj : Function.Injective ⇑h
⊢ Function.Injective ⇑((map S f g) h)

Tactic:
intro x y
  obtain ⟨⟨x, s⟩, rfl⟩ := IsLocalizedModule.mk'_surjective S f x
  obtain ⟨⟨y, t⟩, rfl⟩ := IsLocalizedModule.mk'_surjective S f y
  simp only [Function.uncurry_apply_pair, map_mk', mk'_eq_mk'_iff, Subtype.exists,
    Submonoid.mk_smul, exists_prop, forall_exists_index, and_imp]
  intro c hc e
  exact ⟨c, hc, h_inj (by simpa)⟩

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
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)
i k : J
f : i ⟶ k
g : j ⟶ k
lh : IsLocalHom (Hom.hom (F.map f))
eq :
  (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (c.π.app i)) x) =
    (ConcreteCategory.hom (F.map g)) ((ConcreteCategory.hom (c.π.app j)) x)
⊢ IsUnit ((ConcreteCategory.hom (c.π.app i)) x)

Tactic:
exact lh.map_nonunit _ (eq ▸ hx.map _)

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Oplax

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : B ⥤ᵒᵖᴸ C
G : C ⥤ᵒᵖᴸ D
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ (F.comp G.toPrelaxFunctor).map₂ (ρ_ f).hom =
    ((G.mapFunctor (F.obj a✝) (F.obj b✝)).map (F.mapComp f (𝟙 b✝)) ≫ G.mapComp (F.map f) (F.map (𝟙 b✝))) ≫
      (F.comp G.toPrelaxFunctor).map f ◁ ((G.mapFunctor (F.obj b✝) (F.obj b✝)).map (F.mapId b✝) ≫ G.mapId (F.obj b✝)) ≫
        (ρ_ ((F.comp G.toPrelaxFunctor).map f)).hom

Tactic:
by
    dsimp
    simp only [map₂_rightUnitor, PrelaxFunctor.map₂_comp, mapComp_naturality_right_assoc,
      whiskerLeft_comp, assoc]

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
e : J ≌ K
inst✝ : IsConnected J
⊢ Nonempty J

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case mpr
R : Type w₁
A : Type w₂
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ (∃ ι x f, Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG) → FinitePresentation R A

Tactic:
· rintro ⟨ι, hfintype, f, hf⟩
    have equiv := MvPolynomial.renameEquiv R (Fintype.equivFin ι)
    use Fintype.card ι, f.comp equiv.symm, hf.1.comp (AlgEquiv.symm equiv).surjective
    refine Ideal.fg_ker_comp (S := MvPolynomial ι R) (A := A) _ f ?_ hf.2 equiv.symm.surjective
    simpa using! Submodule.fg_bot

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
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 (ι ⊕ ι')
⊢ Fintype (ι ⊕ ι')

Tactic:
by infer_instance

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

Goal state before:
pp: A : Type u_1
inst✝⁶ : Category.{v_1, u_1} A
B : Type u_2
inst✝⁵ : Category.{v_2, u_2} B
T : Type u_3
inst✝⁴ : Category.{v_3, u_3} T
L : A ⥤ T
R : B ⥤ T
P : MorphismProperty T
Q : MorphismProperty A
W : MorphismProperty B
inst✝³ : Q.IsMultiplicative
inst✝² : W.IsMultiplicative
inst✝¹ : Q.RespectsIso
inst✝ : W.RespectsIso
A✝ B✝ : MorphismProperty.Comma L R P Q W
f : A✝ ⟶ B✝
hf : IsIso ((forget L R P Q W).map f)
⊢ IsIso f

Tactic:
simp only [forget_obj, forget_map] at hf

Goal state after:
A : Type u_1
inst✝⁶ : Category.{v_1, u_1} A
B : Type u_2
inst✝⁵ : Category.{v_2, u_2} B
T : Type u_3
inst✝⁴ : Category.{v_3, u_3} T
L : A ⥤ T
R : B ⥤ T
P : MorphismProperty T
Q : MorphismProperty A
W : MorphismProperty B
inst✝³ : Q.IsMultiplicative
inst✝² : W.IsMultiplicative
inst✝¹ : Q.RespectsIso
inst✝ : W.RespectsIso
A✝ B✝ : MorphismProperty.Comma L R P Q W
f : A✝ ⟶ B✝
hf : IsIso (Hom.hom f)
⊢ IsIso f