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

Goal state before:
pp: case h_zero
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f f' : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ (a : X ⟶ Y), (sum g fun g' t ↦ single (a ≫ g') (0 * t)) = 0

pp: case h_add
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f f' : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ (a : X ⟶ Y) (b₁ b₂ : R),
    (sum g fun g' t ↦ single (a ≫ g') ((b₁ + b₂) * t)) =
      (sum g fun g' t ↦ single (a ≫ g') (b₁ * t)) + sum g fun g' t ↦ single (a ≫ g') (b₂ * t)

Tactic:
<;>

Goal state after:
case h_zero
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f f' : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ (a : X ⟶ Y), (sum g fun g' t ↦ single (a ≫ g') (0 * t)) = 0

case h_add
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f f' : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ (a : X ⟶ Y) (b₁ b₂ : R),
    (sum g fun g' t ↦ single (a ≫ g') ((b₁ + b₂) * t)) =
      (sum g fun g' t ↦ single (a ≫ g') (b₁ * t)) + sum g fun g' t ↦ single (a ≫ g') (b₂ * t)
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: case e_g.h_zero
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
g g' : Y ⟶ Z
r : X ⟶ Y
h : R
a✝ : X ⟶ Z
⊢ ∀ (a : Y ⟶ Z), single (r ≫ a) (h * 0) = 0

pp: case e_g.h_add
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
g g' : Y ⟶ Z
r : X ⟶ Y
h : R
a✝ : X ⟶ Z
⊢ ∀ (a : Y ⟶ Z) (b₁ b₂ : R), single (r ≫ a) (h * (b₁ + b₂)) = single (r ≫ a) (h * b₁) + single (r ≫ a) (h * b₂)

Tactic:
<;>

Goal state after:
case e_g.h_zero
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
g g' : Y ⟶ Z
r : X ⟶ Y
h : R
a✝ : X ⟶ Z
⊢ ∀ (a : Y ⟶ Z), single (r ≫ a) (h * 0) = 0

case e_g.h_add
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
g g' : Y ⟶ Z
r : X ⟶ Y
h : R
a✝ : X ⟶ Z
⊢ ∀ (a : Y ⟶ Z) (b₁ b₂ : R), single (r ≫ a) (h * (b₁ + b₂)) = single (r ≫ a) (h * b₁) + single (r ≫ a) (h * b₂)
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
X Y Z : Free R C
r : R
f : X ⟶ Y
g : Y ⟶ Z
⊢ (sum f fun i a ↦ sum g fun g' t ↦ single (i ≫ g') (r * a * t)) =
    r • sum f fun f' s ↦ sum g fun g' t ↦ single (f' ≫ g') (s * t)

pp: R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
r : R
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ (i : X ⟶ Y), (sum g fun g' t ↦ single (i ≫ g') (0 * t)) = 0

Tactic:
<;>

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
r : R
f : X ⟶ Y
g : Y ⟶ Z
⊢ (sum f fun i a ↦ sum g fun g' t ↦ single (i ≫ g') (r * a * t)) =
    r • sum f fun f' s ↦ sum g fun g' t ↦ single (f' ≫ g') (s * t)

R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
r : R
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ (i : X ⟶ Y), (sum g fun g' t ↦ single (i ≫ g') (0 * t)) = 0
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: case e_g
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
r : R
g : Y ⟶ Z
h : X ⟶ Y
s : R
a✝ : X ⟶ Z
⊢ (sum g fun i a ↦ single (h ≫ i) (s * (r * a))) a✝ = (sum g fun a b ↦ r • single (h ≫ a) (s * b)) a✝

pp: case e_g
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
r : R
g : Y ⟶ Z
h : X ⟶ Y
s : R
a✝ : X ⟶ Z
⊢ ∀ (i : Y ⟶ Z), single (h ≫ i) (s * 0) = 0

Tactic:
<;>

Goal state after:
case e_g
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
r : R
g : Y ⟶ Z
h : X ⟶ Y
s : R
a✝ : X ⟶ Z
⊢ (sum g fun i a ↦ single (h ≫ i) (s * (r * a))) a✝ = (sum g fun a b ↦ r • single (h ≫ a) (s * b)) a✝

case e_g
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
r : R
g : Y ⟶ Z
h : X ⟶ Y
s : R
a✝ : X ⟶ Z
⊢ ∀ (i : Y ⟶ Z), single (h ≫ i) (s * 0) = 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
⊢ S.v₀₁.τ₂ ≫ S.v₁₂.τ₂ = 0

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

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

Goal state before:
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.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: case fst
X Y S : Type v
f : X ⟶ S
g : Y ⟶ S
c : PullbackCone f g
hc : IsLimit c
x y : c.pt
h₁ : (hom c.fst) x = (hom c.fst) y
h₂ : (hom c.snd) x = (hom c.snd) y
⊢ (↑((equivPullbackObj hc) x)).1 = (↑((equivPullbackObj hc) y)).1

pp: case snd
X Y S : Type v
f : X ⟶ S
g : Y ⟶ S
c : PullbackCone f g
hc : IsLimit c
x y : c.pt
h₁ : (hom c.fst) x = (hom c.fst) y
h₂ : (hom c.snd) x = (hom c.snd) y
⊢ (↑((equivPullbackObj hc) x)).2 = (↑((equivPullbackObj hc) y)).2

Tactic:
<;>

Goal state after:
case fst
X Y S : Type v
f : X ⟶ S
g : Y ⟶ S
c : PullbackCone f g
hc : IsLimit c
x y : c.pt
h₁ : (hom c.fst) x = (hom c.fst) y
h₂ : (hom c.snd) x = (hom c.snd) y
⊢ (↑((equivPullbackObj hc) x)).1 = (↑((equivPullbackObj hc) y)).1

case snd
X Y S : Type v
f : X ⟶ S
g : Y ⟶ S
c : PullbackCone f g
hc : IsLimit c
x y : c.pt
h₁ : (hom c.fst) x = (hom c.fst) y
h₂ : (hom c.snd) x = (hom c.snd) y
⊢ (↑((equivPullbackObj hc) x)).2 = (↑((equivPullbackObj hc) y)).2
Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory

Goal state before:
pp: case none
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
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₀ : (hom (base f)) x = (hom (base f)) y
h : ∀ (j : ι), (hom (π f j)) x = (hom (π f j)) y
⊢ (hom (limit.π (wideCospan B X f) none)) x = (hom (limit.π (wideCospan B X f) none)) y

pp: case some
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
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₀ : (hom (base f)) x = (hom (base f)) y
h : ∀ (j : ι), (hom (π f j)) x = (hom (π f j)) y
j : ι
⊢ (hom (limit.π (wideCospan B X f) (some j))) x = (hom (limit.π (wideCospan B X f) (some j))) y

Tactic:
· exact h₀

Goal state after:
case some
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
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₀ : (hom (base f)) x = (hom (base f)) y
h : ∀ (j : ι), (hom (π f j)) x = (hom (π f j)) y
j : ι
⊢ (hom (limit.π (wideCospan B X f) (some j))) x = (hom (limit.π (wideCospan B X f) (some j))) y
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: case fst
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₁ y₁ : X₁
h₁ : (hom t) x₁ = (hom t) y₁
h₂ : (hom l) x₁ = (hom l) y₁
⊢ (↑((h.isLimit.conePointUniqueUpToIso
              ((pullbackCone r b).isLimitAux (fun s ↦ ↾fun x ↦ ⟨((hom s.fst) x, (hom s.snd) x), ⋯⟩) ⋯ ⋯ ⋯)).toEquiv
          x₁)).1 =
    (↑((h.isLimit.conePointUniqueUpToIso
              ((pullbackCone r b).isLimitAux (fun s ↦ ↾fun x ↦ ⟨((hom s.fst) x, (hom s.snd) x), ⋯⟩) ⋯ ⋯ ⋯)).toEquiv
          y₁)).1

pp: case snd
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₁ y₁ : X₁
h₁ : (hom t) x₁ = (hom t) y₁
h₂ : (hom l) x₁ = (hom l) y₁
⊢ (↑((h.isLimit.conePointUniqueUpToIso
              ((pullbackCone r b).isLimitAux (fun s ↦ ↾fun x ↦ ⟨((hom s.fst) x, (hom s.snd) x), ⋯⟩) ⋯ ⋯ ⋯)).toEquiv
          x₁)).2 =
    (↑((h.isLimit.conePointUniqueUpToIso
              ((pullbackCone r b).isLimitAux (fun s ↦ ↾fun x ↦ ⟨((hom s.fst) x, (hom s.snd) x), ⋯⟩) ⋯ ⋯ ⋯)).toEquiv
          y₁)).2

Tactic:
<;>

Goal state after:
case fst
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₁ y₁ : X₁
h₁ : (hom t) x₁ = (hom t) y₁
h₂ : (hom l) x₁ = (hom l) y₁
⊢ (↑((h.isLimit.conePointUniqueUpToIso
              ((pullbackCone r b).isLimitAux (fun s ↦ ↾fun x ↦ ⟨((hom s.fst) x, (hom s.snd) x), ⋯⟩) ⋯ ⋯ ⋯)).toEquiv
          x₁)).1 =
    (↑((h.isLimit.conePointUniqueUpToIso
              ((pullbackCone r b).isLimitAux (fun s ↦ ↾fun x ↦ ⟨((hom s.fst) x, (hom s.snd) x), ⋯⟩) ⋯ ⋯ ⋯)).toEquiv
          y₁)).1

case snd
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₁ y₁ : X₁
h₁ : (hom t) x₁ = (hom t) y₁
h₂ : (hom l) x₁ = (hom l) y₁
⊢ (↑((h.isLimit.conePointUniqueUpToIso
              ((pullbackCone r b).isLimitAux (fun s ↦ ↾fun x ↦ ⟨((hom s.fst) x, (hom s.snd) x), ⋯⟩) ⋯ ⋯ ⋯)).toEquiv
          x₁)).2 =
    (↑((h.isLimit.conePointUniqueUpToIso
              ((pullbackCone r b).isLimitAux (fun s ↦ ↾fun x ↦ ⟨((hom s.fst) x, (hom s.snd) x), ⋯⟩) ⋯ ⋯ ⋯)).toEquiv
          y₁)).2
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: case left
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
w : t ≫ r = l ≫ b
h₁ : ∀ (x₁ y₁ : (fun X ↦ X) X₁), (hom t) x₁ = (hom t) y₁ ∧ (hom l) x₁ = (hom l) y₁ → x₁ = y₁
h₂ : ∀ (x₂ : (fun X ↦ X) X₂) (x₃ : (fun X ↦ X) X₃), (hom r) x₂ = (hom b) x₃ → ∃ x₁, (hom t) x₁ = x₂ ∧ (hom l) x₁ = x₃
φ : X₁ ⟶ PullbackObj r b := ⋯
⊢ Function.Injective ⇑(hom φ)

pp: case right
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
w : t ≫ r = l ≫ b
h₁ : ∀ (x₁ y₁ : (fun X ↦ X) X₁), (hom t) x₁ = (hom t) y₁ ∧ (hom l) x₁ = (hom l) y₁ → x₁ = y₁
h₂ : ∀ (x₂ : (fun X ↦ X) X₂) (x₃ : (fun X ↦ X) X₃), (hom r) x₂ = (hom b) x₃ → ∃ x₁, (hom t) x₁ = x₂ ∧ (hom l) x₁ = x₃
φ : X₁ ⟶ PullbackObj r b := ⋯
⊢ Function.Surjective ⇑(hom φ)

Tactic:
· intro _ _ h
        simp [φ] at h
        grind

Goal state after:
case right
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
w : t ≫ r = l ≫ b
h₁ : ∀ (x₁ y₁ : (fun X ↦ X) X₁), (hom t) x₁ = (hom t) y₁ ∧ (hom l) x₁ = (hom l) y₁ → x₁ = y₁
h₂ : ∀ (x₂ : (fun X ↦ X) X₂) (x₃ : (fun X ↦ X) X₃), (hom r) x₂ = (hom b) x₃ → ∃ x₁, (hom t) x₁ = x₂ ∧ (hom l) x₁ = x₃
φ : X₁ ⟶ PullbackObj r b := ⋯
⊢ Function.Surjective ⇑(hom φ)
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case false.false
property✝ : (false, false) ∈ {x | x.1 < x.2}
⊢ ⟨(false, false), property✝⟩ = ⟨(decide False, decide True), instUniqueLOfLinearOrderBool._proof_1⟩

pp: case false.true
property✝ : (false, true) ∈ {x | x.1 < x.2}
⊢ ⟨(false, true), property✝⟩ = ⟨(decide False, decide True), instUniqueLOfLinearOrderBool._proof_1⟩

pp: case true.false
property✝ : (true, false) ∈ {x | x.1 < x.2}
⊢ ⟨(true, false), property✝⟩ = ⟨(decide False, decide True), instUniqueLOfLinearOrderBool._proof_1⟩

pp: case true.true
property✝ : (true, true) ∈ {x | x.1 < x.2}
⊢ ⟨(true, true), property✝⟩ = ⟨(decide False, decide True), instUniqueLOfLinearOrderBool._proof_1⟩

Tactic:
<;>

Goal state after:
case false.false
property✝ : (false, false) ∈ {x | x.1 < x.2}
⊢ ⟨(false, false), property✝⟩ = ⟨(decide False, decide True), instUniqueLOfLinearOrderBool._proof_1⟩

case false.true
property✝ : (false, true) ∈ {x | x.1 < x.2}
⊢ ⟨(false, true), property✝⟩ = ⟨(decide False, decide True), instUniqueLOfLinearOrderBool._proof_1⟩

case true.false
property✝ : (true, false) ∈ {x | x.1 < x.2}
⊢ ⟨(true, false), property✝⟩ = ⟨(decide False, decide True), instUniqueLOfLinearOrderBool._proof_1⟩

case true.true
property✝ : (true, true) ∈ {x | x.1 < x.2}
⊢ ⟨(true, true), property✝⟩ = ⟨(decide False, decide True), instUniqueLOfLinearOrderBool._proof_1⟩
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left.left.id
J : MulticospanShape
a✝ : J.L
⊢ (Hom.id (left a✝)).comp (Hom.id (left a✝)) = Hom.id (left a✝)

pp: case left.right.fst
J : MulticospanShape
a✝ : J.R
⊢ (Hom.id (left (J.fst a✝))).comp (Hom.fst a✝) = Hom.fst a✝

pp: case left.right.snd
J : MulticospanShape
a✝ : J.R
⊢ (Hom.id (left (J.snd a✝))).comp (Hom.snd a✝) = Hom.snd a✝

pp: case right.right.id
J : MulticospanShape
a✝ : J.R
⊢ (Hom.id (right a✝)).comp (Hom.id (right a✝)) = Hom.id (right a✝)

Tactic:
<;>

Goal state after:
case left.left.id
J : MulticospanShape
a✝ : J.L
⊢ (Hom.id (left a✝)).comp (Hom.id (left a✝)) = Hom.id (left a✝)

case left.right.fst
J : MulticospanShape
a✝ : J.R
⊢ (Hom.id (left (J.fst a✝))).comp (Hom.fst a✝) = Hom.fst a✝

case left.right.snd
J : MulticospanShape
a✝ : J.R
⊢ (Hom.id (left (J.snd a✝))).comp (Hom.snd a✝) = Hom.snd a✝

case right.right.id
J : MulticospanShape
a✝ : J.R
⊢ (Hom.id (right a✝)).comp (Hom.id (right a✝)) = Hom.id (right a✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left.left.id
J : MulticospanShape
a✝ : J.L
⊢ (Hom.id (left a✝)).comp (Hom.id (left a✝)) = Hom.id (left a✝)

pp: case left.right.fst
J : MulticospanShape
a✝ : J.R
⊢ (Hom.fst a✝).comp (Hom.id (right a✝)) = Hom.fst a✝

pp: case left.right.snd
J : MulticospanShape
a✝ : J.R
⊢ (Hom.snd a✝).comp (Hom.id (right a✝)) = Hom.snd a✝

pp: case right.right.id
J : MulticospanShape
a✝ : J.R
⊢ (Hom.id (right a✝)).comp (Hom.id (right a✝)) = Hom.id (right a✝)

Tactic:
<;>

Goal state after:
case left.left.id
J : MulticospanShape
a✝ : J.L
⊢ (Hom.id (left a✝)).comp (Hom.id (left a✝)) = Hom.id (left a✝)

case left.right.fst
J : MulticospanShape
a✝ : J.R
⊢ (Hom.fst a✝).comp (Hom.id (right a✝)) = Hom.fst a✝

case left.right.snd
J : MulticospanShape
a✝ : J.R
⊢ (Hom.snd a✝).comp (Hom.id (right a✝)) = Hom.snd a✝

case right.right.id
J : MulticospanShape
a✝ : J.R
⊢ (Hom.id (right a✝)).comp (Hom.id (right a✝)) = Hom.id (right a✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left
J : MulticospanShape
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : WalkingMulticospan J ⥤ C
left : ∀ (i : J.L), F.obj (WalkingMulticospan.left i) = G.obj (WalkingMulticospan.left i)
right : ∀ (i : J.R), F.obj (WalkingMulticospan.right i) = G.obj (WalkingMulticospan.right i)
wl : ∀ (i : J.R), F.map (Hom.fst i) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ G.map (Hom.fst i)
wr : ∀ (i : J.R), F.map (Hom.snd i) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ G.map (Hom.snd i)
a✝ : J.L
⊢ F.obj (WalkingMulticospan.left a✝) = G.obj (WalkingMulticospan.left a✝)

pp: case right
J : MulticospanShape
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : WalkingMulticospan J ⥤ C
left : ∀ (i : J.L), F.obj (WalkingMulticospan.left i) = G.obj (WalkingMulticospan.left i)
right : ∀ (i : J.R), F.obj (WalkingMulticospan.right i) = G.obj (WalkingMulticospan.right i)
wl : ∀ (i : J.R), F.map (Hom.fst i) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ G.map (Hom.fst i)
wr : ∀ (i : J.R), F.map (Hom.snd i) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ G.map (Hom.snd i)
a✝ : J.R
⊢ F.obj (WalkingMulticospan.right a✝) = G.obj (WalkingMulticospan.right a✝)

Tactic:
<;>

Goal state after:
case left
J : MulticospanShape
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : WalkingMulticospan J ⥤ C
left : ∀ (i : J.L), F.obj (WalkingMulticospan.left i) = G.obj (WalkingMulticospan.left i)
right : ∀ (i : J.R), F.obj (WalkingMulticospan.right i) = G.obj (WalkingMulticospan.right i)
wl : ∀ (i : J.R), F.map (Hom.fst i) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ G.map (Hom.fst i)
wr : ∀ (i : J.R), F.map (Hom.snd i) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ G.map (Hom.snd i)
a✝ : J.L
⊢ F.obj (WalkingMulticospan.left a✝) = G.obj (WalkingMulticospan.left a✝)

case right
J : MulticospanShape
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : WalkingMulticospan J ⥤ C
left : ∀ (i : J.L), F.obj (WalkingMulticospan.left i) = G.obj (WalkingMulticospan.left i)
right : ∀ (i : J.R), F.obj (WalkingMulticospan.right i) = G.obj (WalkingMulticospan.right i)
wl : ∀ (i : J.R), F.map (Hom.fst i) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ G.map (Hom.fst i)
wr : ∀ (i : J.R), F.map (Hom.snd i) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ G.map (Hom.snd i)
a✝ : J.R
⊢ F.obj (WalkingMulticospan.right a✝) = G.obj (WalkingMulticospan.right a✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left
J : MulticospanShape
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : WalkingMulticospan J ⥤ C
left : ∀ (i : J.L), F.obj (WalkingMulticospan.left i) = G.obj (WalkingMulticospan.left i)
right : ∀ (i : J.R), F.obj (WalkingMulticospan.right i) = G.obj (WalkingMulticospan.right i)
wl : ∀ (i : J.R), F.map (Hom.fst i) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ G.map (Hom.fst i)
wr : ∀ (i : J.R), F.map (Hom.snd i) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ G.map (Hom.snd i)
a✝ : J.L
⊢ (functorExt (fun x ↦ eqToIso ⋯) (fun x ↦ eqToIso ⋯) wl wr).hom.app (WalkingMulticospan.left a✝) = eqToHom ⋯

pp: case right
J : MulticospanShape
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : WalkingMulticospan J ⥤ C
left : ∀ (i : J.L), F.obj (WalkingMulticospan.left i) = G.obj (WalkingMulticospan.left i)
right : ∀ (i : J.R), F.obj (WalkingMulticospan.right i) = G.obj (WalkingMulticospan.right i)
wl : ∀ (i : J.R), F.map (Hom.fst i) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ G.map (Hom.fst i)
wr : ∀ (i : J.R), F.map (Hom.snd i) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ G.map (Hom.snd i)
a✝ : J.R
⊢ (functorExt (fun x ↦ eqToIso ⋯) (fun x ↦ eqToIso ⋯) wl wr).hom.app (WalkingMulticospan.right a✝) = eqToHom ⋯

Tactic:
<;>

Goal state after:
case left
J : MulticospanShape
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : WalkingMulticospan J ⥤ C
left : ∀ (i : J.L), F.obj (WalkingMulticospan.left i) = G.obj (WalkingMulticospan.left i)
right : ∀ (i : J.R), F.obj (WalkingMulticospan.right i) = G.obj (WalkingMulticospan.right i)
wl : ∀ (i : J.R), F.map (Hom.fst i) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ G.map (Hom.fst i)
wr : ∀ (i : J.R), F.map (Hom.snd i) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ G.map (Hom.snd i)
a✝ : J.L
⊢ (functorExt (fun x ↦ eqToIso ⋯) (fun x ↦ eqToIso ⋯) wl wr).hom.app (WalkingMulticospan.left a✝) = eqToHom ⋯

case right
J : MulticospanShape
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : WalkingMulticospan J ⥤ C
left : ∀ (i : J.L), F.obj (WalkingMulticospan.left i) = G.obj (WalkingMulticospan.left i)
right : ∀ (i : J.R), F.obj (WalkingMulticospan.right i) = G.obj (WalkingMulticospan.right i)
wl : ∀ (i : J.R), F.map (Hom.fst i) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ G.map (Hom.fst i)
wr : ∀ (i : J.R), F.map (Hom.snd i) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ G.map (Hom.snd i)
a✝ : J.R
⊢ (functorExt (fun x ↦ eqToIso ⋯) (fun x ↦ eqToIso ⋯) wl wr).hom.app (WalkingMulticospan.right a✝) = eqToHom ⋯
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left
J : MultispanShape
inst✝¹ : Small.{t, w} J.L
inst✝ : Small.{t, w'} J.R
a✝ : J.L
⊢ ∃ a, Sum.elim left right a = left a✝

pp: case right
J : MultispanShape
inst✝¹ : Small.{t, w} J.L
inst✝ : Small.{t, w'} J.R
a✝ : J.R
⊢ ∃ a, Sum.elim left right a = right a✝

Tactic:
<;>

Goal state after:
case left
J : MultispanShape
inst✝¹ : Small.{t, w} J.L
inst✝ : Small.{t, w'} J.R
a✝ : J.L
⊢ ∃ a, Sum.elim left right a = left a✝

case right
J : MultispanShape
inst✝¹ : Small.{t, w} J.L
inst✝ : Small.{t, w'} J.R
a✝ : J.R
⊢ ∃ a, Sum.elim left right a = right a✝
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left.left.id
J : MultispanShape
a✝ : J.L
⊢ (Hom.id (left a✝)).comp (Hom.id (left a✝)) = Hom.id (left a✝)

pp: case left.right.fst
J : MultispanShape
a✝ : J.L
⊢ (Hom.id (left a✝)).comp (Hom.fst a✝) = Hom.fst a✝

pp: case left.right.snd
J : MultispanShape
a✝ : J.L
⊢ (Hom.id (left a✝)).comp (Hom.snd a✝) = Hom.snd a✝

pp: case right.right.id
J : MultispanShape
a✝ : J.R
⊢ (Hom.id (right a✝)).comp (Hom.id (right a✝)) = Hom.id (right a✝)

Tactic:
<;>

Goal state after:
case left.left.id
J : MultispanShape
a✝ : J.L
⊢ (Hom.id (left a✝)).comp (Hom.id (left a✝)) = Hom.id (left a✝)

case left.right.fst
J : MultispanShape
a✝ : J.L
⊢ (Hom.id (left a✝)).comp (Hom.fst a✝) = Hom.fst a✝

case left.right.snd
J : MultispanShape
a✝ : J.L
⊢ (Hom.id (left a✝)).comp (Hom.snd a✝) = Hom.snd a✝

case right.right.id
J : MultispanShape
a✝ : J.R
⊢ (Hom.id (right a✝)).comp (Hom.id (right a✝)) = Hom.id (right a✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left.left.id
J : MultispanShape
a✝ : J.L
⊢ (Hom.id (left a✝)).comp (Hom.id (left a✝)) = Hom.id (left a✝)

pp: case left.right.fst
J : MultispanShape
a✝ : J.L
⊢ (Hom.fst a✝).comp (Hom.id (right (J.fst a✝))) = Hom.fst a✝

pp: case left.right.snd
J : MultispanShape
a✝ : J.L
⊢ (Hom.snd a✝).comp (Hom.id (right (J.snd a✝))) = Hom.snd a✝

pp: case right.right.id
J : MultispanShape
a✝ : J.R
⊢ (Hom.id (right a✝)).comp (Hom.id (right a✝)) = Hom.id (right a✝)

Tactic:
<;>

Goal state after:
case left.left.id
J : MultispanShape
a✝ : J.L
⊢ (Hom.id (left a✝)).comp (Hom.id (left a✝)) = Hom.id (left a✝)

case left.right.fst
J : MultispanShape
a✝ : J.L
⊢ (Hom.fst a✝).comp (Hom.id (right (J.fst a✝))) = Hom.fst a✝

case left.right.snd
J : MultispanShape
a✝ : J.L
⊢ (Hom.snd a✝).comp (Hom.id (right (J.snd a✝))) = Hom.snd a✝

case right.right.id
J : MultispanShape
a✝ : J.R
⊢ (Hom.id (right a✝)).comp (Hom.id (right a✝)) = Hom.id (right a✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left
J : MultispanShape
a✝ : J.L
⊢ Sum.elim left right
      ((fun x ↦
          match x with
          | left a => Sum.inl a
          | right b => Sum.inr b)
        (left a✝)) =
    left a✝

pp: case right
J : MultispanShape
a✝ : J.R
⊢ Sum.elim left right
      ((fun x ↦
          match x with
          | left a => Sum.inl a
          | right b => Sum.inr b)
        (right a✝)) =
    right a✝

Tactic:
<;>

Goal state after:
case left
J : MultispanShape
a✝ : J.L
⊢ Sum.elim left right
      ((fun x ↦
          match x with
          | left a => Sum.inl a
          | right b => Sum.inr b)
        (left a✝)) =
    left a✝

case right
J : MultispanShape
a✝ : J.R
⊢ Sum.elim left right
      ((fun x ↦
          match x with
          | left a => Sum.inl a
          | right b => Sum.inr b)
        (right a✝)) =
    right a✝