-- 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
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s✝ : S
z₂ : X₂
hyz : ∃ s, f s✝ = f s ∧ z₂ = g s
⊢ Rel' f g (Sum.inr (g s✝)) (Sum.inr z₂)

Tactic:
obtain ⟨s, hs, rfl⟩ := hyz

Result:
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))

Proof state:
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

Tactic:
obtain z₁|z₂ := z

Result:
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.inr (g s)) (Sum.inl z₁)
⊢ Rel' f g (Sum.inl (f s)) (Sum.inl z₁)

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₂)

Proof state:
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

Tactic:
obtain z₁|z₂ := z

Result:
case inr_inl.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 (f s✝)) (Sum.inl z₁)
⊢ Rel' f g (Sum.inr (g s✝)) (Sum.inl z₁)

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

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

Tactic:
apply Rel'.inl_inr

Result:
no goals

Proof state:
case inl_inl.inl
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 : f y₀✝ = z₁ ∨ ∃ x₀ y₀, ∃ (_ : g x₀ = g y₀), f y₀✝ = f x₀ ∧ z₁ = f y₀
⊢ Rel' f g (Sum.inl (f x₀✝)) (Sum.inl z₁)

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

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

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✝¹ w✝ : S
h' : g w✝¹ = g w✝
h'' : f y₀✝ = f w✝¹
⊢ Rel' f g (Sum.inl (f x₀✝)) (Sum.inl (f w✝))

Proof state:
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✝))

Tactic:
apply Rel'.refl

Result:
no goals

Proof state:
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

Tactic:
obtain z₁|z₂ := z

Result:
case inl_inl.inl
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.inl z₁)
⊢ Rel' f g (Sum.inl (f x₀✝)) (Sum.inl z₁)

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₂)

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 : Rel' f g (Sum.inl (f s✝)) (Sum.inl z₁)
⊢ Rel' f g (Sum.inr (g s✝)) (Sum.inl z₁)

Tactic:
rw [inl_rel'_inl_iff] at hyz

Result:
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₁)

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 : ∃ s, f y₀✝ = f s ∧ z₂ = g s
⊢ Rel' f g (Sum.inl (f x₀✝)) (Sum.inr z₂)

Tactic:
obtain ⟨s, hs, rfl⟩ := hyz

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

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

Tactic:
rw [inl_rel'_inr_iff] at hyz

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

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.inr (g s)) (Sum.inl z₁)
⊢ Rel' f g (Sum.inl (f s)) (Sum.inl z₁)

Tactic:
replace hyz := hyz.symm

Result:
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₁)

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

Tactic:
rw [← h]

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

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

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

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

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

Tactic:
exact Rel'.inl_inl _ _ h

Result:
no goals

Proof state:
case inl_inl.inl
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.inl z₁)
⊢ Rel' f g (Sum.inl (f x₀✝)) (Sum.inl z₁)

Tactic:
rw [inl_rel'_inl_iff] at hyz

Result:
case inl_inl.inl
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 : f y₀✝ = z₁ ∨ ∃ x₀ y₀, ∃ (_ : g x₀ = g y₀), f y₀✝ = f x₀ ∧ z₁ = f y₀
⊢ Rel' f g (Sum.inl (f x₀✝)) (Sum.inl 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✝¹ w✝ : S
h' : g w✝¹ = g w✝
h'' : f y₀✝ = f w✝¹
⊢ Rel' f g (Sum.inl (f x₀✝)) (Sum.inl (f w✝))

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

Result:
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✝))

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 : ∃ s_1, z₁ = f s_1 ∧ g s = g s_1
⊢ Rel' f g (Sum.inl (f s)) (Sum.inl z₁)

Tactic:
obtain ⟨s', rfl, hs'⟩ := hyz

Result:
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'))

Proof state:
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

Tactic:
exact hyz

Result:
no goals