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

Goal state before:
pp: case add.h_zero
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
g : Y ⟶ Z
f₁ f₂ : (X ⟶ Y) →₀ R
w₁ : (sum (f₁ ≫ g) fun f' r ↦ r • F.map f') = (f₁.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
w₂ : (sum (f₂ ≫ g) fun f' r ↦ r • F.map f') = (f₂.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
a✝ : X ⟶ Z
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case single.add
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f' : X ⟶ Y
r : R
f₁ f₂ : (Y ⟶ Z) →₀ R
w₁ :
  (sum (single f' r ≫ f₁) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₁.sum fun f' r ↦ r • F.map f'
w₂ :
  (sum (single f' r ≫ f₂) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₂.sum fun f' r ↦ r • F.map f'
⊢ (sum (single f' r ≫ f₁ + single f' r ≫ f₂) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ (f₁ + f₂).sum fun f' r ↦ r • F.map f'

Tactic:
]

Goal state after:
case single.add
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f' : X ⟶ Y
r : R
f₁ f₂ : (Y ⟶ Z) →₀ R
w₁ :
  (sum (single f' r ≫ f₁) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₁.sum fun f' r ↦ r • F.map f'
w₂ :
  (sum (single f' r ≫ f₂) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₂.sum fun f' r ↦ r • F.map f'
⊢ (sum (single f' r ≫ f₁ + single f' r ≫ f₂) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ (f₁ + f₂).sum fun f' r ↦ r • F.map f'
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.v₀₁.τ₁ ≫ S.v₁₂.τ₁ = 0

Tactic:
rw [← comp_τ₁, S.w₀₂, zero_τ₁]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.v₁₂.τ₂ ≫ S.v₂₃.τ₂ = 0

Tactic:
rw [← comp_τ₂, S.w₁₃, zero_τ₂]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.v₀₁.τ₃ ≫ S.v₁₂.τ₃ = 0

Tactic:
by rw [← comp_τ₃, S.w₀₂, zero_τ₃]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
S : SnakeInput C
inst✝ : Mono S.L₁.f
⊢ Mono (S.v₀₁.τ₁ ≫ S.L₁.f)

Tactic:
]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
S : SnakeInput C
inst✝ : Mono S.L₁.f
⊢ Mono (S.v₀₁.τ₁ ≫ S.L₁.f)
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
S : SnakeInput C
inst✝ : Epi S.L₂.g
⊢ Epi (S.L₂.g ≫ S.v₂₃.τ₃)

Tactic:
]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
S : SnakeInput C
inst✝ : Epi S.L₂.g
⊢ Epi (S.L₂.g ≫ S.v₂₃.τ₃)
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ ∀ ⦃A : C⦄ (x₂ : A ⟶ S.L₀.X₂), x₂ ≫ S.L₀.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.L₀.f

Tactic:
]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ ∀ ⦃A : C⦄ (x₂ : A ⟶ S.L₀.X₂), x₂ ≫ S.L₀.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.L₀.f
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
A : C
x₂ : A ⟶ S.L₀.X₂
hx₂ : x₂ ≫ S.L₀.g = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ ∀ ⦃A : C⦄ (x₂ : A ⟶ S.L₀'.X₂), x₂ ≫ S.L₀'.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.L₀'.f

Tactic:
]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ ∀ ⦃A : C⦄ (x₂ : A ⟶ S.L₀'.X₂), x₂ ≫ S.L₀'.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.L₀'.f
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
A : C
x₂ : A ⟶ S.P
hx₂ : x₂ ≫ pullback.snd S.L₁.g S.v₀₁.τ₃ = 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case single.add.h_zero
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f' : X ⟶ Y
r : R
f₁ f₂ : (Y ⟶ Z) →₀ R
w₁ :
  (sum (single f' r ≫ f₁) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₁.sum fun f' r ↦ r • F.map f'
w₂ :
  (sum (single f' r ≫ f₂) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₂.sum fun f' r ↦ r • F.map f'
a✝ : Y ⟶ Z
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ ∀ ⦃A : C⦄ (x₂ : A ⟶ S.L₁'.X₂), x₂ ≫ S.L₁'.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.L₁'.f

Tactic:
]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ ∀ ⦃A : C⦄ (x₂ : A ⟶ S.L₁'.X₂), x₂ ≫ S.L₁'.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.L₁'.f
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: case single.add.h_zero
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f' : X ⟶ Y
r : R
f₁ f₂ : (Y ⟶ Z) →₀ R
w₁ :
  (sum (single f' r ≫ f₁) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₁.sum fun f' r ↦ r • F.map f'
w₂ :
  (sum (single f' r ≫ f₂) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₂.sum fun f' r ↦ r • F.map f'
a✝ : X ⟶ Z
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
A₀ : C
x₃ : A₀ ⟶ S.L₀.X₃
hx₃ : x₃ ≫ S.δ = 0
A₁ : C
π₁ : A₁ ⟶ A₀
hπ₁ : Epi π₁
p : A₁ ⟶ S.P
hp : π₁ ≫ x₃ = p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case single.single
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f' : X ⟶ Y
r : R
g' : Y ⟶ Z
s : R
⊢ ((single (f' ≫ g') (r * s)).sum fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ (single g' s).sum fun f' r ↦ r • F.map f'

Tactic:
]

Goal state after:
case single.single
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f' : X ⟶ Y
r : R
g' : Y ⟶ Z
s : R
⊢ ((single (f' ≫ g') (r * s)).sum fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ (single g' s).sum fun f' r ↦ r • F.map f'
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y : Free R C
f g : X ⟶ Y
⊢ ((sum f fun f' r ↦ r • F.map f') + sum g fun f' r ↦ r • F.map f') =
    (sum f fun f' r ↦ r • F.map f') + sum g fun f' r ↦ r • F.map f'

pp: case h_zero
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y : Free R C
f g : X ⟶ Y
⊢ ∀ (a : X ⟶ Y), 0 • F.map a = 0

pp: case h_add
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y : Free R C
f g : X ⟶ Y
⊢ ∀ (a : X ⟶ Y) (b₁ b₂ : R), (b₁ + b₂) • F.map a = b₁ • F.map a + b₂ • F.map a

Tactic:
]

Goal state after:
case h_zero
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y : Free R C
f g : X ⟶ Y
⊢ ∀ (a : X ⟶ Y), 0 • F.map a = 0

case h_add
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y : Free R C
f g : X ⟶ Y
⊢ ∀ (a : X ⟶ Y) (b₁ b₂ : R), (b₁ + b₂) • F.map a = b₁ • F.map a + b₂ • F.map a
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y : Free R C
f : X ⟶ Y
r : R
⊢ (sum f fun i a ↦ (r * a) • F.map i) = r • sum f fun f' r ↦ r • F.map f'

pp: R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y : Free R C
f : X ⟶ Y
r : R
⊢ ∀ (i : X ⟶ Y), 0 • F.map i = 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y : Free R C
f : X ⟶ Y
r : R
⊢ (sum f fun i a ↦ (r * a) • F.map i) = r • sum f fun f' r ↦ r • F.map f'

R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y : Free R C
f : X ⟶ Y
r : R
⊢ ∀ (i : X ⟶ Y), 0 • F.map i = 0
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ (pushout.inr S.L₁.g.op S.v₀₁.τ₃.op).unop ≫ S.op.δ.unop ≫ (pullback.snd S.L₂.f.op S.v₂₃.τ₁.op).unop =
    (pushout.inl S.L₁.g.op S.v₀₁.τ₃.op).unop ≫ S.v₁₂.τ₂ ≫ (pullback.fst S.L₂.f.op S.v₂₃.τ₁.op).unop

Tactic:
]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ (pushout.inr S.L₁.g.op S.v₀₁.τ₃.op).unop ≫ S.op.δ.unop ≫ (pullback.snd S.L₂.f.op S.v₂₃.τ₁.op).unop =
    (pushout.inl S.L₁.g.op S.v₀₁.τ₃.op).unop ≫ S.v₁₂.τ₂ ≫ (pullback.fst S.L₂.f.op S.v₂₃.τ₁.op).unop
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.op.L₁'.Exact

Tactic:
]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.op.L₁'.Exact
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
A : C
x₃ : A ⟶ S.L₀.X₃
x₂ : A ⟶ S.L₁.X₂
x₁ : A ⟶ S.L₂.X₁
h₂ : x₂ ≫ S.L₁.g = x₃ ≫ S.v₀₁.τ₃
h₁ : x₁ ≫ S.L₂.f = x₂ ≫ S.v₁₂.τ₂
H : x₃ ≫ S.δ = pullback.lift x₂ x₃ h₂ ≫ S.φ₁ ≫ S.v₂₃.τ₁
⊢ x₃ ≫ S.δ = x₁ ≫ S.v₂₃.τ₁

Tactic:
]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
A : C
x₃ : A ⟶ S.L₀.X₃
x₂ : A ⟶ S.L₁.X₂
x₁ : A ⟶ S.L₂.X₁
h₂ : x₂ ≫ S.L₁.g = x₃ ≫ S.v₀₁.τ₃
h₁ : x₁ ≫ S.L₂.f = x₂ ≫ S.v₁₂.τ₂
H : x₃ ≫ S.δ = pullback.lift x₂ x₃ h₂ ≫ S.φ₁ ≫ S.v₂₃.τ₁
⊢ x₃ ≫ S.δ = x₁ ≫ S.v₂₃.τ₁
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
A : C
x₃ : A ⟶ S.L₀.X₃
x₂ : A ⟶ S.L₁.X₂
x₁ : A ⟶ S.L₂.X₁
h₂ : x₂ ≫ S.L₁.g = x₃ ≫ S.v₀₁.τ₃
h₁ : x₁ ≫ S.L₂.f = x₂ ≫ S.v₁₂.τ₂
H : x₃ ≫ S.δ = pullback.lift x₂ x₃ h₂ ≫ S.φ₁ ≫ S.v₂₃.τ₁
⊢ (pullback.lift x₂ x₃ h₂ ≫ S.φ₁) ≫ S.v₂₃.τ₁ = x₁ ≫ S.v₂₃.τ₁

Tactic:
]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
A : C
x₃ : A ⟶ S.L₀.X₃
x₂ : A ⟶ S.L₁.X₂
x₁ : A ⟶ S.L₂.X₁
h₂ : x₂ ≫ S.L₁.g = x₃ ≫ S.v₀₁.τ₃
h₁ : x₁ ≫ S.L₂.f = x₂ ≫ S.v₁₂.τ₂
H : x₃ ≫ S.δ = pullback.lift x₂ x₃ h₂ ≫ S.φ₁ ≫ S.v₂₃.τ₁
⊢ (pullback.lift x₂ x₃ h₂ ≫ S.φ₁) ≫ S.v₂₃.τ₁ = x₁ ≫ S.v₂₃.τ₁
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S S₁ S₂ S₃ : SnakeInput C
f : S₁.Hom S₂
g : S₂.Hom S₃
⊢ (f.f₁ ≫ g.f₁) ≫ S₃.v₁₂ = S₁.v₁₂ ≫ f.f₂ ≫ g.f₂

Tactic:
simp only [assoc, comm₁₂, comm₁₂_assoc]

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

Goal state before:
pp: case add
R : Type u_1
inst✝⁸ : CommRing R
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u
inst✝⁶ : Category.{v, u} D
inst✝⁵ : Preadditive D
inst✝⁴ : Linear R D
F G : Free R C ⥤ D
inst✝³ : F.Additive
inst✝² : Functor.Linear R F
inst✝¹ : G.Additive
inst✝ : Functor.Linear R G
α : embedding R C ⋙ F ≅ embedding R C ⋙ G
X Y : Free R C
f₁ f₂ : (X ⟶ Y) →₀ R
w₁ : F.map f₁ ≫ (α.app Y).hom = (α.app X).hom ≫ G.map f₁
w₂ : F.map f₂ ≫ (α.app Y).hom = (α.app X).hom ≫ G.map f₂
⊢ (α.app X).hom ≫ G.map f₁ + (α.app X).hom ≫ G.map f₂ = (α.app X).hom ≫ G.map f₁ + (α.app X).hom ≫ G.map f₂

Tactic:
]

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

Goal state before:
pp: case single
R : Type u_1
inst✝⁸ : CommRing R
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u
inst✝⁶ : Category.{v, u} D
inst✝⁵ : Preadditive D
inst✝⁴ : Linear R D
F G : Free R C ⥤ D
inst✝³ : F.Additive
inst✝² : Functor.Linear R F
inst✝¹ : G.Additive
inst✝ : Functor.Linear R G
α : embedding R C ⋙ F ≅ embedding R C ⋙ G
X Y : Free R C
f' : X ⟶ Y
r : R
⊢ r • F.map (single f' 1) ≫ α.hom.app Y = r • α.hom.app X ≫ G.map (single f' 1)

Tactic:
]

Goal state after:
case single
R : Type u_1
inst✝⁸ : CommRing R
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u
inst✝⁶ : Category.{v, u} D
inst✝⁵ : Preadditive D
inst✝⁴ : Linear R D
F G : Free R C ⥤ D
inst✝³ : F.Additive
inst✝² : Functor.Linear R F
inst✝¹ : G.Additive
inst✝ : Functor.Linear R G
α : embedding R C ⋙ F ≅ embedding R C ⋙ G
X Y : Free R C
f' : X ⟶ Y
r : R
⊢ r • F.map (single f' 1) ≫ α.hom.app Y = r • α.hom.app X ≫ G.map (single f' 1)
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : SnakeInput C
f : S₁ ⟶ S₂
⊢ pullback.snd S₁.L₁.g S₁.v₀₁.τ₃ ≫ f.f₀.τ₃ ≫ S₂.δ = pullback.snd S₁.L₁.g S₁.v₀₁.τ₃ ≫ f.f₀.τ₃ ≫ S₂.δ

Tactic:
]

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

Goal state before:
pp: case single
R : Type u_1
inst✝⁸ : CommRing R
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u
inst✝⁶ : Category.{v, u} D
inst✝⁵ : Preadditive D
inst✝⁴ : Linear R D
F G : Free R C ⥤ D
inst✝³ : F.Additive
inst✝² : Functor.Linear R F
inst✝¹ : G.Additive
inst✝ : Functor.Linear R G
α : embedding R C ⋙ F ≅ embedding R C ⋙ G
X Y : Free R C
f' : X ⟶ Y
r : R
⊢ r • α.hom.app X ≫ (embedding R C ⋙ G).map f' = r • α.hom.app X ≫ (embedding R C ⋙ G).map f'

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max w v)
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : Type w
F : J → C
inst✝¹ : HasProduct F
inst✝ : PreservesLimit (Discrete.functor F) (forget C)
x : (j : J) → ToType (F j)
j : J
⊢ x j = x j

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
f : J → C
inst✝⁷ : HasProduct f
D : Type t
inst✝⁶ : Category.{r, t} D
FD : D → D → Type u_1
DD : D → Type (max w r)
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (DD X) (DD Y)
inst✝⁴ : ConcreteCategory D FD
F : C ⥤ D
inst✝³ : PreservesLimit (Discrete.functor f) F
inst✝² : HasProduct fun j ↦ F.obj (f j)
inst✝¹ : PreservesLimitsOfShape WalkingCospan (forget D)
inst✝ : PreservesLimit (Discrete.functor fun b ↦ F.obj (f b)) (forget D)
x y : ToType (F.obj (∏ᶜ f))
h : ∀ (i : J), (hom (F.map (Pi.π f i))) x = (hom (F.map (Pi.π f i))) y
j : J
⊢ (hom (F.map (Pi.π f j))) x = (hom (F.map (Pi.π f j))) y

Tactic:
]

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
f : J → C
inst✝⁷ : HasProduct f
D : Type t
inst✝⁶ : Category.{r, t} D
FD : D → D → Type u_1
DD : D → Type (max w r)
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (DD X) (DD Y)
inst✝⁴ : ConcreteCategory D FD
F : C ⥤ D
inst✝³ : PreservesLimit (Discrete.functor f) F
inst✝² : HasProduct fun j ↦ F.obj (f j)
inst✝¹ : PreservesLimitsOfShape WalkingCospan (forget D)
inst✝ : PreservesLimit (Discrete.functor fun b ↦ F.obj (f b)) (forget D)
x y : ToType (F.obj (∏ᶜ f))
h : ∀ (i : J), (hom (F.map (Pi.π f i))) x = (hom (F.map (Pi.π f i))) y
j : J
⊢ (hom (F.map (Pi.π f j))) x = (hom (F.map (Pi.π f j))) y
Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
inst✝ : PreservesColimit (Functor.empty C) (forget C)
X : C
h : Nonempty (IsInitial X)
⊢ Nonempty (IsInitial (ToType X))

Tactic:
]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
inst✝ : PreservesColimit (Functor.empty C) (forget C)
X : C
h : Nonempty (IsInitial X)
⊢ Nonempty (IsInitial (ToType X))
Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
inst✝¹ : PreservesColimit (Functor.empty C) (forget C)
inst✝ : ReflectsColimit (Functor.empty C) (forget C)
X : C
⊢ Nonempty (IsInitial ((forget C).obj X)) ↔ Nonempty (IsInitial (ToType X))

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: P X Y Z : Type u
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
e : P ≅ PullbackObj f g := h.isoPullback ≪≫ pullbackIsoPullback f g
p : (fun X ↦ X) P
⊢ (hom fst) p = (hom fst) p

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: P X Y Z : Type u
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
e : P ≅ PullbackObj f g := h.isoPullback ≪≫ pullbackIsoPullback f g
this : ⇑(hom fst) = _root_.Prod.fst ∘ Subtype.val ∘ ⇑(hom e.hom)
⊢ _root_.Prod.fst '' Subtype.val '' Set.univ = ⇑(hom f) ⁻¹' Set.range ⇑(hom g)

Tactic:
]

Goal state after:
P X Y Z : Type u
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
e : P ≅ PullbackObj f g := h.isoPullback ≪≫ pullbackIsoPullback f g
this : ⇑(hom fst) = _root_.Prod.fst ∘ Subtype.val ∘ ⇑(hom e.hom)
⊢ _root_.Prod.fst '' Subtype.val '' Set.univ = ⇑(hom f) ⁻¹' Set.range ⇑(hom g)
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: P X Y Z : Type u
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
⊢ ⇑(hom g) ⁻¹' Set.range ⇑(hom f) = ⇑(hom g) ⁻¹' Set.range ⇑(hom f)

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max v w)
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
B : C
ι : Type w
inst✝² : Nonempty ι
X : ι → C
f : (j : ι) → X j ⟶ B
inst✝¹ : HasWidePullback B X f
inst✝ : PreservesLimit (wideCospan B X f) (forget C)
x y : ToType (widePullback B X f)
h : ∀ (j : ι), (hom (π f j)) x = (hom (π f j)) y
⊢ x = y

Tactic:
by
  apply Concrete.widePullback_ext _ _ _ _ h
  inhabit ι
  simp only [← π_arrow f default, ConcreteCategory.comp_apply, h]

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

Goal state before:
pp: case right
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
inst✝¹ : HasMultiequalizer I
inst✝ : PreservesLimit I.multicospan (forget C)
x y : ToType (multiequalizer I)
h : ∀ (t : J.L), (hom (Multiequalizer.ι I t)) x = (hom (Multiequalizer.ι I t)) y
b : J.R
⊢ (hom (I.multicospan.map (WalkingMulticospan.Hom.fst b)))
      ((hom (limit.π I.multicospan (WalkingMulticospan.left (J.fst b)))) x) =
    (hom (I.multicospan.map (WalkingMulticospan.Hom.fst b)))
      ((hom (limit.π I.multicospan (WalkingMulticospan.left (J.fst b)))) y)

Tactic:
]

Goal state after:
case right
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
inst✝¹ : HasMultiequalizer I
inst✝ : PreservesLimit I.multicospan (forget C)
x y : ToType (multiequalizer I)
h : ∀ (t : J.L), (hom (Multiequalizer.ι I t)) x = (hom (Multiequalizer.ι I t)) y
b : J.R
⊢ (hom (I.multicospan.map (WalkingMulticospan.Hom.fst b)))
      ((hom (limit.π I.multicospan (WalkingMulticospan.left (J.fst b)))) x) =
    (hom (I.multicospan.map (WalkingMulticospan.Hom.fst b)))
      ((hom (limit.π I.multicospan (WalkingMulticospan.left (J.fst b)))) y)
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h : IsPullback t l r b
x₂ : X₂
x₃ : X₃
hx : (hom r) x₂ = (hom b) x₃
x₁ : h.cone.pt
hx₁ : ↑((PullbackCone.IsLimit.equivPullbackObj h.isLimit) x₁) = ↑⟨(x₂, x₃), hx⟩
⊢ ∃ x₁, (hom t) x₁ = x₂ ∧ (hom l) x₁ = x₃

Tactic:
]

Goal state after:
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h : IsPullback t l r b
x₂ : X₂
x₃ : X₃
hx : (hom r) x₂ = (hom b) x₃
x₁ : h.cone.pt
hx₁ : ↑((PullbackCone.IsLimit.equivPullbackObj h.isLimit) x₁) = ↑⟨(x₂, x₃), hx⟩
⊢ ∃ x₁, (hom t) x₁ = x₂ ∧ (hom l) x₁ = x₃