mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ (PushoutCocone.mk f g ⋯).inl ≫ m = s.inl →
    (PushoutCocone.mk f g ⋯).inr ≫ m = s.inr → m = BinaryCofan.IsColimit.desc H₂ s.inl s.inr

Tactic:
h₁

Goal state after:
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
⊢ (PushoutCocone.mk f g ⋯).inr ≫ m = s.inr → m = BinaryCofan.IsColimit.desc H₂ s.inl s.inr
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 //
    l ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst ∧
      l ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt},
          m ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst → m ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd → m = l }

Tactic:
obtain ⟨l₁, hl₁, hl₁'⟩ := PullbackCone.IsLimit.lift' H' s.fst l₂ (by rw [← hl₂, hi₂])

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₂
⊢ { l //
    l ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst ∧
      l ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt},
          m ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst → m ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd → m = l }
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case refine_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst✝¹ : HasBinaryProduct A X
inst✝ : HasBinaryProduct B X
s : PullbackCone f prod.fst
m : s.pt ⟶ (PullbackCone.mk prod.fst (prod.map f (𝟙 X)) ⋯).pt
⊢ m ≫ (PullbackCone.mk prod.fst (prod.map f (𝟙 X)) ⋯).fst = s.fst →
    m ≫ (PullbackCone.mk prod.fst (prod.map f (𝟙 X)) ⋯).snd = s.snd → m = prod.lift s.fst (s.snd ≫ prod.snd)

Tactic:
h₁

Goal state after:
case refine_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst✝¹ : HasBinaryProduct A X
inst✝ : HasBinaryProduct B X
s : PullbackCone f prod.fst
m : s.pt ⟶ (PullbackCone.mk prod.fst (prod.map f (𝟙 X)) ⋯).pt
h₁ : m ≫ (PullbackCone.mk prod.fst (prod.map f (𝟙 X)) ⋯).fst = s.fst
⊢ m ≫ (PullbackCone.mk prod.fst (prod.map f (𝟙 X)) ⋯).snd = s.snd → m = prod.lift s.fst (s.snd ≫ prod.snd)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case mp
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : M × ↥S
u : ↥S
v : R
h₁ : u • b.1 = v • a.1
h₂ : ↑u * ↑b.2 = v * ↑a.2
⊢ r S M a b

Tactic:
use u

Goal state after:
case h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : M × ↥S
u : ↥S
v : R
h₁ : u • b.1 = v • a.1
h₂ : ↑u * ↑b.2 = v * ↑a.2
⊢ u • b.2 • a.1 = u • a.2 • b.1
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case refine_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst✝¹ : HasBinaryCoproduct A X
inst✝ : HasBinaryCoproduct B X
s : PushoutCocone coprod.inl f
m : (PushoutCocone.mk (coprod.map f (𝟙 X)) coprod.inl ⋯).pt ⟶ s.pt
⊢ (PushoutCocone.mk (coprod.map f (𝟙 X)) coprod.inl ⋯).inl ≫ m = s.inl →
    (PushoutCocone.mk (coprod.map f (𝟙 X)) coprod.inl ⋯).inr ≫ m = s.inr → m = coprod.desc s.inr (coprod.inr ≫ s.inl)

Tactic:
h₁

Goal state after:
case refine_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst✝¹ : HasBinaryCoproduct A X
inst✝ : HasBinaryCoproduct B X
s : PushoutCocone coprod.inl f
m : (PushoutCocone.mk (coprod.map f (𝟙 X)) coprod.inl ⋯).pt ⟶ s.pt
h₁ : (PushoutCocone.mk (coprod.map f (𝟙 X)) coprod.inl ⋯).inl ≫ m = s.inl
⊢ (PushoutCocone.mk (coprod.map f (𝟙 X)) coprod.inl ⋯).inr ≫ m = s.inr → m = coprod.desc s.inr (coprod.inr ≫ s.inl)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
⊢ IsLimit (Fork.ofι f ⋯)

Tactic:
fapply Fork.IsLimit.mk

Goal state after:
case lift
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
⊢ (s : Fork g g') → s.pt ⟶ (Fork.ofι f ⋯).pt

case fac
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
⊢ ∀ (s : Fork g g'), ?lift s ≫ (Fork.ofι f ⋯).ι = s.ι

case uniq
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
⊢ ∀ (s : Fork g g') (m : s.pt ⟶ (Fork.ofι f ⋯).pt), m ≫ (Fork.ofι f ⋯).ι = s.ι → m = ?lift s
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:
simp only [Submonoid.map_powers, Algebra.TensorProduct.includeRight_apply]

Goal state after:
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.powers (1 ⊗ₜ[R] g)) (Localization.Away (1 ⊗ₜ[R] g))
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h
R : Type u
inst✝¹⁰ : CommSemiring R
S✝ : Submonoid R
M : Type v
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
T : Type u_1
inst✝⁷ : CommSemiring T
inst✝⁶ : Algebra R T
inst✝⁵ : IsLocalization S✝ T
T' : Type u_2
inst✝⁴ : CommSemiring T'
inst✝³ : Algebra R T'
inst✝² : IsLocalization S✝ T'
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Submonoid R
a✝ : LocalizedModule S A
a₁ : A
s₁ : ↥S
b✝ : LocalizedModule S A
a₂ : A
s₂ : ↥S
c✝ : LocalizedModule S A
a₃ : A
s₃ : ↥S
⊢ 1 • (s₁ * s₃ * (s₂ * s₃)) • ((s₂ • a₁ + s₁ • a₂) * a₃) =
    1 • (s₁ * s₂ * s₃) • ((s₂ * s₃) • (a₁ * a₃) + (s₁ * s₃) • (a₂ * a₃))

Tactic:
simp only [one_mul, smul_add, add_mul, smul_smul, ← mul_assoc, smul_mul_assoc,
        mul_right_comm]

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:
simp only [Submonoid.map_powers, Algebra.TensorProduct.includeRight_apply]

Goal state after:
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.powers (1 ⊗ₜ[R] g)) (Localization.Away (1 ⊗ₜ[R] g))
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u
inst✝⁸ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
T : Type u_1
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : IsLocalization S T
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
t : T
t' : T'
p : LocalizedModule S M
⊢ t • t' • p = t' • t • p

Tactic:
induction p with

Goal state after:
case h
R : Type u
inst✝⁸ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
T : Type u_1
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : IsLocalization S T
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
t : T
t' : T'
m : M
s : ↥S
⊢ t • t' • mk m s = t' • t • mk m s
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
p : LocalizedModule S M
⊢ 1 • p = p

Tactic:
induction p with

Goal state after:
case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
m : M
s : ↥S
⊢ 1 • mk m s = mk m s
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x y : T
p : LocalizedModule S M
⊢ (x * y) • p = x • y • p

Tactic:
induction p with

Goal state after:
case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x y : T
m : M
s : ↥S
⊢ (x * y) • mk m s = x • y • mk m s
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Quiver.IsThin C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
⊢ IsPullback fst snd f g ↔ Nonempty (IsLimit (BinaryFan.mk fst snd))

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · exact ⟨BinaryFan.IsLimit.mk _ (fun u v ↦ h.lift u v (by subsingleton))
      (by subsingleton) (by subsingleton) (by subsingleton)⟩
  · exact ⟨⟨by subsingleton⟩,
      ⟨PullbackCone.IsLimit.mk _ (fun s ↦ BinaryFan.IsLimit.lift h.some s.fst s.snd)
      (by subsingleton) (by subsingleton) (by subsingleton)⟩⟩

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

Goal state before:
pp: R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x : T
p q : LocalizedModule S M
⊢ x • (p + q) = x • p + x • q

Tactic:
induction p with

Goal state after:
case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x : T
q : LocalizedModule S M
m : M
s : ↥S
⊢ x • (mk m s + q) = x • mk m s + x • q
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x y : T
p : LocalizedModule S M
⊢ (x + y) • p = x • p + y • p

Tactic:
induction p with

Goal state after:
case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x y : T
m : M
s : ↥S
⊢ (x + y) • mk m s = x • mk m s + y • mk m s
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
p : LocalizedModule S M
⊢ 0 • p = 0

Tactic:
induction p with

Goal state after:
case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
m : M
s : ↥S
⊢ 0 • mk m s = 0
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u
inst✝⁸ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
T : Type u_1
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : IsLocalization S T
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
r : R
x : T
p : LocalizedModule S M
⊢ (r • x) • p = r • x • p

Tactic:
induction p with

Goal state after:
case h
R : Type u
inst✝⁸ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
T : Type u_1
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : IsLocalization S T
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
r : R
x : T
m : M
s : ↥S
⊢ (r • x) • mk m s = r • x • mk m s
Module: Mathlib.CategoryTheory.Monad.Basic

Goal state before:
pp: case a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Monad C
i : T.toFunctor ≅ F
X : C
| T.η.app (F.obj X) ≫ T.map (i.inv.app X)

pp: case a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Monad C
i : T.toFunctor ≅ F
X : C
| T.μ.app X

pp: case a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Monad C
i : T.toFunctor ≅ F
X : C
| i.hom.app X

Tactic:
← T.η.naturality (i.inv.app X),

Goal state after:
case a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Monad C
i : T.toFunctor ≅ F
X : C
| (𝟭 C).map (i.inv.app X) ≫ T.η.app (T.obj X)

case a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Monad C
i : T.toFunctor ≅ F
X : C
| T.μ.app X

case a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Monad C
i : T.toFunctor ≅ F
X : C
| i.hom.app X
Module: Mathlib.CategoryTheory.Monad.Basic

Goal state before:
pp: case a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Comonad C
i : T.toFunctor ≅ F
X : C
| T.δ.app X ≫ T.map (T.ε.app X)

pp: case a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Comonad C
i : T.toFunctor ≅ F
X : C
| i.hom.app ((𝟭 C).obj X)

pp: case a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Comonad C
i : T.toFunctor ≅ F
X : C
| i.inv.app X

Tactic:
rw [T.right_counit]

Goal state after:
case a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Comonad C
i : T.toFunctor ≅ F
X : C
| 𝟙 (T.obj X)

case a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Comonad C
i : T.toFunctor ≅ F
X : C
| i.hom.app ((𝟭 C).obj X)

case a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Comonad C
i : T.toFunctor ≅ F
X : C
| i.inv.app X
Module: Mathlib.CategoryTheory.Monad.Algebra

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : Comonad C
X : G.Coalgebra
Y : C
g : X ⟶ G.cofree.obj Y
⊢ g.f ≫ (G.cofree.obj Y).a ≫ G.map (G.ε.app Y) = g.f

Tactic:
cofree_obj_a,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : Comonad C
X : G.Coalgebra
Y : C
g : X ⟶ G.cofree.obj Y
⊢ g.f ≫ G.δ.app Y ≫ G.map (G.ε.app Y) = g.f
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case e_a
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)
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ ↑⋯.unit⁻¹ (↑(b * b') • g a') = g (b • a')

Tactic:
· dsimp
        rw [Module.End.algebraMap_isUnit_inv_apply_eq_iff, mul_comm, mul_smul, ← map_smul]
        rfl

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)
x : M
⊢ (lift S g h ∘ₗ mkLinearMap S M) x = g x

Tactic:
simp [LocalizedModule.lift_mk]

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

Goal state before:
pp: case property.right.right
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 := ⋯
f' : A →ₐ[R] ↑s.pt := ⋯
g' : B →ₐ[R] ↑s.pt := ⋯
this : Algebra R ↑(pushoutCocone R A B).pt := ⋯
⊢ ∀ {m : (pushoutCocone R A B).pt ⟶ s.pt},
    ofHom Algebra.TensorProduct.includeLeftRingHom ≫ m = s.inl →
      ofHom Algebra.TensorProduct.includeRight.toRingHom ≫ m = s.inr →
        m = ofHom (Algebra.TensorProduct.productMap f' g').toRingHom

Tactic:
intro h eq1 eq2

Goal state after:
case property.right.right
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
h : (pushoutCocone R A B).pt ⟶ s.pt
eq1 : ofHom Algebra.TensorProduct.includeLeftRingHom ≫ h = s.inl
eq2 : ofHom Algebra.TensorProduct.includeRight.toRingHom ≫ h = s.inr
⊢ h = ofHom (Algebra.TensorProduct.productMap f' g').toRingHom
Module: Mathlib.Algebra.Category.Ring.Constructions

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

Tactic:
hom_ofHom

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
N : Type u_8
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : AddCommGroup N
inst✝ : Module R N
g : M' →ₗ[R] N
H : ∀ (m : M), g (f m) = 0 → f m = 0
x✝ y✝ : M
hxy : g (f x✝) = g (f y✝)
⊢ f x✝ = f y✝

Tactic:
rw [← sub_eq_zero, ← map_sub]

Goal state after:
R : Type u_1
inst✝⁷ : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
N : Type u_8
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : AddCommGroup N
inst✝ : Module R N
g : M' →ₗ[R] N
H : ∀ (m : M), g (f m) = 0 → f m = 0
x✝ y✝ : M
hxy : g (f x✝) = g (f y✝)
⊢ f (x✝ - y✝) = 0
Module: Mathlib.Algebra.Category.Ring.Constructions

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

Tactic:
simpa [CommRingCat.ofHom] using e

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✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
⊢ G.map₂ (F.map₂ (α_ f g h).hom) ≫
      (G.map₂ (F.mapComp f (g ≫ h)) ≫ G.mapComp (F.map f) (F.map (g ≫ h))) ≫
        G.map (F.map f) ◁ (G.map₂ (F.mapComp g h) ≫ G.mapComp (F.map g) (F.map h)) =
    (G.map₂ (F.mapComp (f ≫ g) h) ≫ G.mapComp (F.map (f ≫ g)) (F.map h)) ≫
      (G.map₂ (F.mapComp f g) ≫ G.mapComp (F.map f) (F.map g)) ▷ G.map (F.map h) ≫
        (α_ (G.map (F.map f)) (G.map (F.map g)) (G.map (F.map h))).hom

Tactic:
simp only [map₂_associator, ← PrelaxFunctor.map₂_comp_assoc, ← mapComp_naturality_right_assoc,
      whiskerLeft_comp, assoc]

Goal state after:
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✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
⊢ G.map₂ (F.mapComp (f ≫ g) h ≫ F.mapComp f g ▷ F.map h ≫ (α_ (F.map f) (F.map g) (F.map h)).hom) ≫
      G.mapComp (F.map f) (F.map g ≫ F.map h) ≫ G.map (F.map f) ◁ G.mapComp (F.map g) (F.map h) =
    G.map₂ (F.mapComp (f ≫ g) h) ≫
      G.mapComp (F.map (f ≫ g)) (F.map h) ≫
        (G.map₂ (F.mapComp f g) ≫ G.mapComp (F.map f) (F.map g)) ▷ G.map (F.map h) ≫
          (α_ (G.map (F.map f)) (G.map (F.map g)) (G.map (F.map h))).hom