mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R₁ R₂ R₃ R₄ : Type u₁
inst✝³ : CommRing R₁
inst✝² : CommRing R₂
inst✝¹ : CommRing R₃
inst✝ : CommRing R₄
f₁₂ : R₁ →+* R₂
f₂₃ : R₂ →+* R₃
f₃₄ : R₃ →+* R₄
M : ModuleCat R₁
m : ↑M
h₁ : (ConcreteCategory.hom ((extendScalarsComp (f₂₃.comp f₁₂) f₃₄).hom.app M)) (1 ⊗ₜ[R₁] m) = 1 ⊗ₜ[R₃] (1 ⊗ₜ[R₁] m)
h₂ : (ConcreteCategory.hom ((extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).hom.app M)) (1 ⊗ₜ[R₁] m) = 1 ⊗ₜ[R₂] (1 ⊗ₜ[R₁] m)
h₃ :
  ∀ (M : ModuleCat R₂) (m : ↑M),
    (ConcreteCategory.hom ((extendScalarsComp f₂₃ f₃₄).hom.app M)) (1 ⊗ₜ[R₂] m) = 1 ⊗ₜ[R₃] (1 ⊗ₜ[R₂] m)
h₄ : (ConcreteCategory.hom ((extendScalarsComp f₁₂ f₂₃).hom.app M)) (1 ⊗ₜ[R₁] m) = 1 ⊗ₜ[R₂] (1 ⊗ₜ[R₁] m)
⊢ (Hom.hom ((extendScalars f₃₄).map ((extendScalarsComp f₁₂ f₂₃).hom.app M)))
      ((Hom.hom ((extendScalarsComp (f₂₃.comp f₁₂) f₃₄).hom.app M)) (1 ⊗ₜ[R₁] m)) =
    (Hom.hom ((extendScalarsComp f₂₃ f₃₄).hom.app ((extendScalars f₁₂).obj M)))
      ((Hom.hom ((extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).hom.app M)) (1 ⊗ₜ[R₁] m))

Tactic:
rw [h₁]

Goal state after:
R₁ R₂ R₃ R₄ : Type u₁
inst✝³ : CommRing R₁
inst✝² : CommRing R₂
inst✝¹ : CommRing R₃
inst✝ : CommRing R₄
f₁₂ : R₁ →+* R₂
f₂₃ : R₂ →+* R₃
f₃₄ : R₃ →+* R₄
M : ModuleCat R₁
m : ↑M
h₁ : (ConcreteCategory.hom ((extendScalarsComp (f₂₃.comp f₁₂) f₃₄).hom.app M)) (1 ⊗ₜ[R₁] m) = 1 ⊗ₜ[R₃] (1 ⊗ₜ[R₁] m)
h₂ : (ConcreteCategory.hom ((extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).hom.app M)) (1 ⊗ₜ[R₁] m) = 1 ⊗ₜ[R₂] (1 ⊗ₜ[R₁] m)
h₃ :
  ∀ (M : ModuleCat R₂) (m : ↑M),
    (ConcreteCategory.hom ((extendScalarsComp f₂₃ f₃₄).hom.app M)) (1 ⊗ₜ[R₂] m) = 1 ⊗ₜ[R₃] (1 ⊗ₜ[R₂] m)
h₄ : (ConcreteCategory.hom ((extendScalarsComp f₁₂ f₂₃).hom.app M)) (1 ⊗ₜ[R₁] m) = 1 ⊗ₜ[R₂] (1 ⊗ₜ[R₁] m)
⊢ (Hom.hom ((extendScalars f₃₄).map ((extendScalarsComp f₁₂ f₂₃).hom.app M))) (1 ⊗ₜ[R₃] (1 ⊗ₜ[R₁] m)) =
    (Hom.hom ((extendScalarsComp f₂₃ f₃₄).hom.app ((extendScalars f₁₂).obj M)))
      ((Hom.hom ((extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).hom.app M)) (1 ⊗ₜ[R₁] m))
Module: Mathlib.RingTheory.Coalgebra.TensorProduct

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

Tactic:
by
      ext x y z
      dsimp
      hopf_tensor_induction comul (R := S) x with x₁ x₂
      hopf_tensor_induction comul (R := S) y with y₁ y₂
      hopf_tensor_induction comul (R := R) z with z₁ z₂
      simp

Goal state after:
Module: Mathlib.Algebra.Ring.BooleanRing

Goal state before:
pp: α : Type u_1
inst✝ : BooleanRing α
a : α
⊢ -a = -a + 0

Tactic:
by rw [add_zero]

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.CoassocSimps

Goal state before:
pp: R : Type u_1
M : Type u_3
M' : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Coalgebra R M
f : M →ₗ[R] M'
⊢ (α⁻¹ ∘ₗ f ⊗ₘ δ) ∘ₗ δ = ((LinearMap.rTensor M (LinearMap.rTensor M f) ∘ₗ α⁻¹) ∘ₗ LinearMap.lTensor M δ) ∘ₗ δ

Tactic:
LinearMap.rTensor_def,

Goal state after:
R : Type u_1
M : Type u_3
M' : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Coalgebra R M
f : M →ₗ[R] M'
⊢ (α⁻¹ ∘ₗ f ⊗ₘ δ) ∘ₗ δ = (((f ⊗ₘ LinearMap.id) ⊗ₘ LinearMap.id ∘ₗ α⁻¹) ∘ₗ LinearMap.lTensor M δ) ∘ₗ δ
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: case pos
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b : R
ha : a ≠ 0
h : ∀ (p : R), Prime p → emultiplicity p a ≤ emultiplicity p b
hb : b = 0
⊢ a ∣ b

pp: case neg
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b : R
ha : a ≠ 0
h : ∀ (p : R), Prime p → emultiplicity p a ≤ emultiplicity p b
hb : ¬b = 0
⊢ a ∣ b

Tactic:
· simp_all

Goal state after:
case neg
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b : R
ha : a ≠ 0
h : ∀ (p : R), Prime p → emultiplicity p a ≤ emultiplicity p b
hb : ¬b = 0
⊢ a ∣ b
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: case pos
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b : R
n : ℕ
hn : n ≠ 0
ha : a = 0
⊢ a ^ n ∣ b ^ n ↔ a ∣ b

Tactic:
simp [ha, hn]

Goal state after:
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
inst✝¹ : IsLocalization M S
x : R
e : IsUnit x
inst✝ : Away x S
⊢ Submonoid.closure {x} ≤ IsUnit.submonoid R

Tactic:
Submonoid.closure_le,

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
inst✝¹ : IsLocalization M S
x : R
e : IsUnit x
inst✝ : Away x S
⊢ {x} ⊆ ↑(IsUnit.submonoid R)
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: R : Type u
inst✝ : Ring R
I : Ideal R
r : R
h : r ∈ I.jacobson
s : R
hs : s * 1 * r + s - 1 ∈ I
⊢ ∃ s, s * (r + 1) - 1 ∈ I

Tactic:
use s

Goal state after:
case h
R : Type u
inst✝ : Ring R
I : Ideal R
r : R
h : r ∈ I.jacobson
s : R
hs : s * 1 * r + s - 1 ∈ I
⊢ s * (r + 1) - 1 ∈ I
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_1 : S), ∃ b_1 m, f b_1 = f (a * b) ^ m * a_1
s : S
n : ℕ
⊢ ∃ c l m k, f (a ^ (k + n) * c) = f (a ^ (k + l) * b ^ m) * s

Tactic:
obtain ⟨c, m, e⟩ := H s

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
f : R →+* S
a b : R
H : ∀ (a_1 : S), ∃ b_1 m, f b_1 = f (a * b) ^ m * a_1
s : S
n : ℕ
c : R
m : ℕ
e : f c = f (a * b) ^ m * s
⊢ ∃ c l m k, f (a ^ (k + n) * c) = f (a ^ (k + l) * b ^ m) * s
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: 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 ∉ 𝔪
𝔪₀ : Ideal R := Submodule.comap (DistribSMul.toLinearMap R R (MulOpposite.op r)) 𝔪
I𝔪₀ : I ≤ 𝔪₀
J : Ideal R
b : R
𝔪₀J : 𝔪₀ ≤ J
b𝔪₀ : b ∉ 𝔪₀
bJ : b ∈ J
K : Ideal R := span {b * r} ⊔ 𝔪
s y : R
y𝔪 : y ∈ 𝔪
sbyr : y = r - s * (b * r)
⊢ 1 - s * b ∈ 𝔪₀

Tactic:
rw [sbyr, ← mul_assoc] at y𝔪

Goal state after:
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 ∉ 𝔪
𝔪₀ : Ideal R := Submodule.comap (DistribSMul.toLinearMap R R (MulOpposite.op r)) 𝔪
I𝔪₀ : I ≤ 𝔪₀
J : Ideal R
b : R
𝔪₀J : 𝔪₀ ≤ J
b𝔪₀ : b ∉ 𝔪₀
bJ : b ∈ J
K : Ideal R := span {b * r} ⊔ 𝔪
s y : R
y𝔪 : r - s * b * r ∈ 𝔪
sbyr : y = r - s * (b * r)
⊢ 1 - s * b ∈ 𝔪₀
Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
h : ∀ (A : C) (f : A ⟶ ⊥_ C), IsIso f
I A : C
f : A ⟶ I
hI : IsInitial I
this : IsIso (f ≫ hI.to (⊥_ C))
⊢ f ≫ hI.to (⊥_ C) ≫ inv (f ≫ hI.to (⊥_ C)) = 𝟙 A

Tactic:
by rw [← assoc, IsIso.hom_inv_id]

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

Goal state before:
pp: R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
b : Basis ι R M
m : M
i : ι
this : ↑R ↑(ofIsLocalizedModule Rₛ S f b).repr ∘ₗ f = Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ) ∘ₗ ↑b.repr
⊢ ((ofIsLocalizedModule Rₛ S f b).repr (f m)) i = (algebraMap R Rₛ) ((b.repr m) i)

Tactic:
by
    exact DFunLike.congr_fun (LinearMap.congr_fun this m) i

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
x : M
y : ↥S
⊢ ((map S) f) (mk x y) = mk (f x) y

Tactic:
IsLocalizedModule.mk_eq_mk',

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
x : M
y : ↥S
⊢ ((map S) f) (IsLocalizedModule.mk' (mkLinearMap S M) x y) = mk (f x) y
Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts

Goal state before:
pp: case right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsTerminal Z
H₂ : IsLimit (BinaryFan.mk h k)
s : PullbackCone f g
m : s.pt ⟶ (PullbackCone.mk h k ⋯).pt
h₁ : m ≫ (PullbackCone.mk h k ⋯).fst = s.fst
h₂ : m ≫ (PullbackCone.mk h k ⋯).snd = s.snd
⊢ ∀ (j : Discrete WalkingPair),
    m ≫ (BinaryFan.mk h k).π.app j = BinaryFan.IsLimit.lift H₂ s.fst s.snd ≫ (BinaryFan.mk h k).π.app j

Tactic:
rintro ⟨⟨⟩⟩

Goal state after:
case right.left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsTerminal Z
H₂ : IsLimit (BinaryFan.mk h k)
s : PullbackCone f g
m : s.pt ⟶ (PullbackCone.mk h k ⋯).pt
h₁ : m ≫ (PullbackCone.mk h k ⋯).fst = s.fst
h₂ : m ≫ (PullbackCone.mk h k ⋯).snd = s.snd
⊢ m ≫ (BinaryFan.mk h k).π.app { as := WalkingPair.left } =
    BinaryFan.IsLimit.lift H₂ s.fst s.snd ≫ (BinaryFan.mk h k).π.app { as := WalkingPair.left }

case right.right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsTerminal Z
H₂ : IsLimit (BinaryFan.mk h k)
s : PullbackCone f g
m : s.pt ⟶ (PullbackCone.mk h k ⋯).pt
h₁ : m ≫ (PullbackCone.mk h k ⋯).fst = s.fst
h₂ : m ≫ (PullbackCone.mk h k ⋯).snd = s.snd
⊢ m ≫ (BinaryFan.mk h k).π.app { as := WalkingPair.right } =
    BinaryFan.IsLimit.lift H₂ s.fst s.snd ≫ (BinaryFan.mk h k).π.app { as := WalkingPair.right }
Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts

Goal state before:
pp: case right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsInitial W
H₂ : IsColimit (BinaryCofan.mk f g)
s : PushoutCocone h k
m : (PushoutCocone.mk f g ⋯).pt ⟶ s.pt
h₁ : (PushoutCocone.mk f g ⋯).inl ≫ m = s.inl
h₂ : (PushoutCocone.mk f g ⋯).inr ≫ m = s.inr
⊢ ∀ (j : Discrete WalkingPair),
    (BinaryCofan.mk f g).ι.app j ≫ m = (BinaryCofan.mk f g).ι.app j ≫ BinaryCofan.IsColimit.desc H₂ s.inl s.inr

Tactic:
rintro ⟨⟨⟩⟩

Goal state after:
case right.left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsInitial W
H₂ : IsColimit (BinaryCofan.mk f g)
s : PushoutCocone h k
m : (PushoutCocone.mk f g ⋯).pt ⟶ s.pt
h₁ : (PushoutCocone.mk f g ⋯).inl ≫ m = s.inl
h₂ : (PushoutCocone.mk f g ⋯).inr ≫ m = s.inr
⊢ (BinaryCofan.mk f g).ι.app { as := WalkingPair.left } ≫ m =
    (BinaryCofan.mk f g).ι.app { as := WalkingPair.left } ≫ BinaryCofan.IsColimit.desc H₂ s.inl s.inr

case right.right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsInitial W
H₂ : IsColimit (BinaryCofan.mk f g)
s : PushoutCocone h k
m : (PushoutCocone.mk f g ⋯).pt ⟶ s.pt
h₁ : (PushoutCocone.mk f g ⋯).inl ≫ m = s.inl
h₂ : (PushoutCocone.mk f g ⋯).inr ≫ m = s.inr
⊢ (BinaryCofan.mk f g).ι.app { as := WalkingPair.right } ≫ m =
    (BinaryCofan.mk f g).ι.app { as := WalkingPair.right } ≫ BinaryCofan.IsColimit.desc H₂ s.inl s.inr
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
c : BinaryFan X Y
h : IsLimit c
t : IsTerminal Z
⊢ ∀ (j : Discrete WalkingPair),
    c.π.app j =
      (Iso.refl c.pt).hom ≫
        (BinaryFan.mk (c.π.1 { as := WalkingPair.left }) (c.π.1 { as := WalkingPair.right })).π.app j

Tactic:
rintro ⟨⟨⟩⟩

Goal state after:
case left
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
c : BinaryFan X Y
h : IsLimit c
t : IsTerminal Z
⊢ c.π.app { as := WalkingPair.left } =
    (Iso.refl c.pt).hom ≫
      (BinaryFan.mk (c.π.1 { as := WalkingPair.left }) (c.π.1 { as := WalkingPair.right })).π.app
        { as := WalkingPair.left }

case right
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
c : BinaryFan X Y
h : IsLimit c
t : IsTerminal Z
⊢ c.π.app { as := WalkingPair.right } =
    (Iso.refl c.pt).hom ≫
      (BinaryFan.mk (c.π.1 { as := WalkingPair.left }) (c.π.1 { as := WalkingPair.right })).π.app
        { as := WalkingPair.right }
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y : C
c : BinaryCofan X Y
h : IsColimit c
t : IsInitial Z
⊢ ∀ (j : Discrete WalkingPair),
    c.ι.app j ≫ (Iso.refl c.pt).hom =
      (BinaryCofan.mk (c.ι.1 { as := WalkingPair.left }) (c.ι.1 { as := WalkingPair.right })).ι.app j

Tactic:
rintro ⟨⟨⟩⟩

Goal state after:
case left
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y : C
c : BinaryCofan X Y
h : IsColimit c
t : IsInitial Z
⊢ c.ι.app { as := WalkingPair.left } ≫ (Iso.refl c.pt).hom =
    (BinaryCofan.mk (c.ι.1 { as := WalkingPair.left }) (c.ι.1 { as := WalkingPair.right })).ι.app
      { as := WalkingPair.left }

case right
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y : C
c : BinaryCofan X Y
h : IsColimit c
t : IsInitial Z
⊢ c.ι.app { as := WalkingPair.right } ≫ (Iso.refl c.pt).hom =
    (BinaryCofan.mk (c.ι.1 { as := WalkingPair.left }) (c.ι.1 { as := WalkingPair.right })).ι.app
      { as := WalkingPair.right }
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ Y₁ : C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
i₁ : X₁ ⟶ Y₁
t₁ : PushoutCocone i₁ f₁
i₂ : X₂ ⟶ t₁.pt
t₂ : PushoutCocone «i₂» f₂
hi₂ : «i₂» = t₁.inr
H : IsColimit t₁
H' : IsColimit t₂
⊢ IsColimit (t₁.pasteHoriz t₂ hi₂)

Tactic:
apply PushoutCocone.isColimitAux'
  intro s
  -- Obtain the induced map from descending from both the small squares consecutively.
  obtain ⟨l₁, hl₁, hl₁'⟩ := PushoutCocone.IsColimit.desc' H s.inl (f₂ ≫ s.inr)
    (by rw [s.condition, Category.assoc])
  obtain ⟨l₂, hl₂, hl₂'⟩ := PushoutCocone.IsColimit.desc' H' l₁ s.inr (by rw [← hl₁', hi₂])
  refine ⟨l₂, by simp [hl₂, hl₁], hl₂', ?_⟩
  -- Uniqueness also follows from the universal property of both the small squares.
  intro m hm₁ hm₂
  apply PushoutCocone.IsColimit.hom_ext H' _ (by simpa [hl₂'] using hm₂)
  simp only [PushoutCocone.mk_pt, PushoutCocone.mk_ι_app, Category.assoc] at hm₁ hm₂
  apply PushoutCocone.IsColimit.hom_ext H
  · rw [hm₁, ← hl₁, hl₂]
  · rw [← hi₂, reassoc_of% t₂.condition, reassoc_of% t₂.condition, hm₂, hl₂']

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : ReflectsColimit (span f g) F
e : f ≫ h = g ≫ i
H : IsPushout (F.map f) (F.map g) (F.map h) (F.map i)
⊢ IsColimit (F.mapCocone (PushoutCocone.mk h i ⋯))

Tactic:
refine
    (IsColimit.equivOfNatIsoOfIso (spanCompIso F f g) _ _ (WalkingSpan.ext ?_ ?_ ?_)).symm
      H.isColimit

Goal state after:
case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : ReflectsColimit (span f g) F
e : f ≫ h = g ≫ i
H : IsPushout (F.map f) (F.map g) (F.map h) (F.map i)
⊢ ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone (PushoutCocone.mk h i ⋯))).pt ≅ H.cocone.pt

case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : ReflectsColimit (span f g) F
e : f ≫ h = g ≫ i
H : IsPushout (F.map f) (F.map g) (F.map h) (F.map i)
⊢ ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone (PushoutCocone.mk h i ⋯))).ι.app WalkingCospan.left ≫
      Iso.hom ?refine_1 =
    H.cocone.ι.app WalkingCospan.left

case refine_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : ReflectsColimit (span f g) F
e : f ≫ h = g ≫ i
H : IsPushout (F.map f) (F.map g) (F.map h) (F.map i)
⊢ ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone (PushoutCocone.mk h i ⋯))).ι.app WalkingCospan.right ≫
      Iso.hom ?refine_1 =
    H.cocone.ι.app WalkingCospan.right
Module: Mathlib.Algebra.Group.Submonoid.Units

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup Gˣ
x : Gˣ
⊢ ↑x ∈ H.ofUnits ↔ x ∈ H

Tactic:
mem_ofUnits_iff_toUnits_mem,

Goal state after:
G : Type u_2
inst✝ : Group G
H : Subgroup Gˣ
x : Gˣ
⊢ toUnits ↑x ∈ H ↔ x ∈ H
Module: Mathlib.CategoryTheory.Monad.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G M N : Comonad C
f : M.toFunctor ≅ N.toFunctor
f_ε : ∀ (X : C), f.hom.app X ≫ N.ε.app X = M.ε.app X
f_δ : ∀ (X : C), f.hom.app X ≫ N.δ.app X = M.δ.app X ≫ f.hom.app (M.obj X) ≫ N.map (f.hom.app X)
X : C
⊢ M.δ.app X = M.δ.app X ≫ 𝟙 (M.obj (M.obj X))

Tactic:
apply (comp_id _).symm

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

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_2
inst✝⁹ : AddCommMonoid M
A : Type u_5
inst✝⁸ : CommSemiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Module R M
S : Submonoid R
inst✝⁵ : Module A M
N : Type u_6
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : Module A N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
f : M →ₗ[A] N
h : IsLocalizedModule (Algebra.algebraMapSubmonoid A S) f
y : N
⊢ ∃ x, x.2 • y = (↑R f) x.1

Tactic:
obtain ⟨⟨x, ⟨_, ⟨r, ⟨hr₁, rfl⟩⟩⟩⟩, hx⟩ := h.2 y
    exact ⟨⟨x, ⟨r, hr₁⟩⟩, by simpa [Submonoid.smul_def] using hx⟩

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

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_2
inst✝⁹ : AddCommMonoid M
A : Type u_5
inst✝⁸ : CommSemiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Module R M
S : Submonoid R
inst✝⁵ : Module A M
N : Type u_6
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : Module A N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
f : M →ₗ[A] N
h : IsLocalizedModule (Algebra.algebraMapSubmonoid A S) f
y : N
⊢ ∃ x, x.2 • y = (↑R f) x.1

Tactic:
by
    obtain ⟨⟨x, ⟨_, ⟨r, ⟨hr₁, rfl⟩⟩⟩⟩, hx⟩ := h.2 y
    exact ⟨⟨x, ⟨r, hr₁⟩⟩, by simpa [Submonoid.smul_def] using hx⟩

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✝¹ : HasPushoutsAlong f
inst✝ : ∀ (Z : C) (g : X ⟶ Z), Mono (pushout.inl g f)
⊢ (pushout f).Faithful

Tactic:
have (Z : Under X) : Mono ((mapPushoutAdj f).unit.app Z) := by simp; infer_instance

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y✝ : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst✝¹ : HasPushoutsAlong f
inst✝ : ∀ (Z : C) (g : X ⟶ Z), Mono (pushout.inl g f)
this : ∀ (Z : Under X), Mono ((mapPushoutAdj f).unit.app Z)
⊢ (pushout f).Faithful
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:
mk'_cancel

Goal state after:
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
⊢ f m = f m
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
m' : M'
⊢ mk' f (s • m) s = s • m' ↔ f m = s • m'

Tactic:
mk'_cancel

Goal state after:
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
m' : M'
⊢ f m = s • m' ↔ f m = s • m'
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: A B : CommRingCat
s : BinaryCofan A B
m : ↑A ⊗[ℤ] ↑B →+* ↑s.pt
hm : ∀ (j : Discrete WalkingPair), (A.coproductCocone B).ι.app j ≫ { hom' := m } = s.ι.app j
⊢ ↑(Algebra.TensorProduct.liftEquiv.symm { hom' := m }.hom.toIntAlgHom) =
    ↑(Algebra.TensorProduct.liftEquiv.symm
        (Hom.hom
            (ofHom
              (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom
                  ⋯).toRingHom)).toIntAlgHom)

Tactic:
Algebra.TensorProduct.liftEquiv_symm_apply_coe,

Goal state after:
A B : CommRingCat
s : BinaryCofan A B
m : ↑A ⊗[ℤ] ↑B →+* ↑s.pt
hm : ∀ (j : Discrete WalkingPair), (A.coproductCocone B).ι.app j ≫ { hom' := m } = s.ι.app j
⊢ ({ hom' := m }.hom.toIntAlgHom.comp Algebra.TensorProduct.includeLeft,
      (AlgHom.restrictScalars ℤ { hom' := m }.hom.toIntAlgHom).comp Algebra.TensorProduct.includeRight) =
    ↑(Algebra.TensorProduct.liftEquiv.symm
        (Hom.hom
            (ofHom
              (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom
                  ⋯).toRingHom)).toIntAlgHom)
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:
by
  have : HasLimit (F ⋙ Comma.fst _ _) := i₁
  have : HasLimit (F ⋙ Comma.snd _ _) := i₂
  apply Comma.hasLimit

Goal state after: