-- Mathlib/CategoryTheory/Limits/Shapes/Types.lean
lemma equivalence_rel' [Mono f] : _root_.Equivalence (Rel' f g) where
  refl := Rel'.refl
  symm h := h.symm
  trans

Proof state:
case inr_inl.inr.intro.intro
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s✝ s : S
hs : f s✝ = f s
⊢ Rel' f g (Sum.inr (g s✝)) (Sum.inr (g s))

Tactic:
obtain rfl := (mono_iff_injective f).1 inferInstance hs

Result:
case inr_inl.inr.intro.intro
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s✝ : S
hs : f s✝ = f s✝
⊢ Rel' f g (Sum.inr (g s✝)) (Sum.inr (g s✝))

Proof state:
case inr_inl.inl.inr.intro.intro.intro.intro
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s✝ w✝ : S
h : g s✝ = g w✝
h' : f s✝ = f s✝
⊢ Rel' f g (Sum.inr (g w✝)) (Sum.inl (f w✝))

Tactic:
apply Rel'.inr_inl

Result:
no goals

Proof state:
case inl_inr.inl.intro.intro
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s s' : S
hs' : g s = g s'
⊢ Rel' f g (Sum.inl (f s)) (Sum.inl (f s'))

Tactic:
exact Rel'.inl_inl _ _ hs'

Result:
no goals

Proof state:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
⊢ ∀ {x y z : X₁ ⊕ X₂}, Rel' f g x y → Rel' f g y z → Rel' f g x z

Tactic:
rintro x y z (_|⟨_, _, h⟩|s|_) hyz

Result:
case refl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
x z : X₁ ⊕ X₂
hyz : Rel' f g x z
⊢ Rel' f g x z

case inl_inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
z : X₁ ⊕ X₂
x₀✝ y₀✝ : S
h : g x₀✝ = g y₀✝
hyz : Rel' f g (Sum.inl (f y₀✝)) z
⊢ Rel' f g (Sum.inl (f x₀✝)) z

case inl_inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
z : X₁ ⊕ X₂
s : S
hyz : Rel' f g (Sum.inr (g s)) z
⊢ Rel' f g (Sum.inl (f s)) z

case inr_inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
z : X₁ ⊕ X₂
s✝ : S
hyz : Rel' f g (Sum.inl (f s✝)) z
⊢ Rel' f g (Sum.inr (g s✝)) z

Proof state:
case inr_inl.inl.inr.intro.intro.intro.intro
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s✝ w✝¹ w✝ : S
h : g w✝¹ = g w✝
h' : f s✝ = f w✝¹
⊢ Rel' f g (Sum.inr (g s✝)) (Sum.inl (f w✝))

Tactic:
obtain rfl := (mono_iff_injective f).1 inferInstance h'

Result:
case inr_inl.inl.inr.intro.intro.intro.intro
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s✝ w✝ : S
h : g s✝ = g w✝
h' : f s✝ = f s✝
⊢ Rel' f g (Sum.inr (g s✝)) (Sum.inl (f w✝))

Proof state:
case inl_inr.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s : S
z₂ : X₂
hyz : g s = z₂
⊢ Rel' f g (Sum.inl (f s)) (Sum.inr z₂)

Tactic:
subst hyz

Result:
case inl_inr.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s : S
⊢ Rel' f g (Sum.inl (f s)) (Sum.inr (g s))

Proof state:
case inl_inr.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s : S
⊢ Rel' f g (Sum.inl (f s)) (Sum.inr (g s))

Tactic:
apply Rel'.inl_inr

Result:
no goals

Proof state:
case inr_inl.inl.inr.intro.intro.intro.intro
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s✝ w✝ : S
h : g s✝ = g w✝
h' : f s✝ = f s✝
⊢ Rel' f g (Sum.inr (g s✝)) (Sum.inl (f w✝))

Tactic:
rw [h]

Result:
case inr_inl.inl.inr.intro.intro.intro.intro
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s✝ w✝ : S
h : g s✝ = g w✝
h' : f s✝ = f s✝
⊢ Rel' f g (Sum.inr (g w✝)) (Sum.inl (f w✝))

Proof state:
case inl_inr.inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s : S
z₁ : X₁
hyz : Rel' f g (Sum.inl z₁) (Sum.inr (g s))
⊢ Rel' f g (Sum.inl (f s)) (Sum.inl z₁)

Tactic:
rw [inl_rel'_inr_iff] at hyz

Result:
case inl_inr.inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s : S
z₁ : X₁
hyz : ∃ s_1, z₁ = f s_1 ∧ g s = g s_1
⊢ Rel' f g (Sum.inl (f s)) (Sum.inl z₁)

Proof state:
case inr_inl.inl.inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s✝ : S
⊢ Rel' f g (Sum.inr (g s✝)) (Sum.inl (f s✝))

Tactic:
apply Rel'.inr_inl

Result:
no goals

Proof state:
case inl_inl.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
x₀✝ y₀✝ : S
h : g x₀✝ = g y₀✝
z₂ : X₂
hyz : Rel' f g (Sum.inl (f y₀✝)) (Sum.inr z₂)
⊢ Rel' f g (Sum.inl (f x₀✝)) (Sum.inr z₂)

Tactic:
rw [inl_rel'_inr_iff] at hyz

Result:
case inl_inl.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
x₀✝ y₀✝ : S
h : g x₀✝ = g y₀✝
z₂ : X₂
hyz : ∃ s, f y₀✝ = f s ∧ z₂ = g s
⊢ Rel' f g (Sum.inl (f x₀✝)) (Sum.inr z₂)

Proof state:
case inl_inl.inl.inr.intro.intro.intro.intro
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
x₀✝ y₀✝ : S
h : g x₀✝ = g y₀✝
w✝ : S
h' : g y₀✝ = g w✝
h'' : f y₀✝ = f y₀✝
⊢ Rel' f g (Sum.inl (f x₀✝)) (Sum.inl (f w✝))

Tactic:
exact Rel'.inl_inl _ _ (h.trans h')

Result:
no goals

Proof state:
case inl_inr.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s : S
z₂ : X₂
hyz : Rel' f g (Sum.inr (g s)) (Sum.inr z₂)
⊢ Rel' f g (Sum.inl (f s)) (Sum.inr z₂)

Tactic:
rw [inr_rel'_inr_iff] at hyz

Result:
case inl_inr.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s : S
z₂ : X₂
hyz : g s = z₂
⊢ Rel' f g (Sum.inl (f s)) (Sum.inr z₂)

Proof state:
case inr_inl.inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s✝ : S
z₁ : X₁
hyz : f s✝ = z₁ ∨ ∃ x₀ y₀, ∃ (_ : g x₀ = g y₀), f s✝ = f x₀ ∧ z₁ = f y₀
⊢ Rel' f g (Sum.inr (g s✝)) (Sum.inl z₁)

Tactic:
obtain rfl|⟨_, _, h, h', rfl⟩  := hyz

Result:
case inr_inl.inl.inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s✝ : S
⊢ Rel' f g (Sum.inr (g s✝)) (Sum.inl (f s✝))

case inr_inl.inl.inr.intro.intro.intro.intro
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s✝ w✝¹ w✝ : S
h : g w✝¹ = g w✝
h' : f s✝ = f w✝¹
⊢ Rel' f g (Sum.inr (g s✝)) (Sum.inl (f w✝))