-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
lemma ext_s (s s' : S.Splitting) (h : s.s = s'.s) : s = s'

Proof state:
case mk.mk
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
this : Mono S.f
r✝ : S.X₂ ⟶ S.X₁
s✝ : S.X₃ ⟶ S.X₂
f_r✝¹ : S.f ≫ r✝ = 𝟙 S.X₁
s_g✝¹ : s✝ ≫ S.g = 𝟙 S.X₃
id✝¹ : r✝ ≫ S.f + S.g ≫ s✝ = 𝟙 S.X₂
f_r✝ : S.f ≫ { r := r✝, s := s✝, f_r := f_r✝¹, s_g := s_g✝¹, id := id✝¹ }.r = 𝟙 S.X₁
s_g✝ : { r := r✝, s := s✝, f_r := f_r✝¹, s_g := s_g✝¹, id := id✝¹ }.s ≫ S.g = 𝟙 S.X₃
id✝ :
  { r := r✝, s := s✝, f_r := f_r✝¹, s_g := s_g✝¹, id := id✝¹ }.r ≫ S.f +
      S.g ≫ { r := r✝, s := s✝, f_r := f_r✝¹, s_g := s_g✝¹, id := id✝¹ }.s =
    𝟙 S.X₂
⊢ { r := r✝, s := s✝, f_r := f_r✝¹, s_g := s_g✝¹, id := id✝¹ } =
    { r := { r := r✝, s := s✝, f_r := f_r✝¹, s_g := s_g✝¹, id := id✝¹ }.r,
      s := { r := r✝, s := s✝, f_r := f_r✝¹, s_g := s_g✝¹, id := id✝¹ }.s, f_r := f_r✝, s_g := s_g✝, id := id✝ }

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
s s' : S.Splitting
h : s.s = s'.s
⊢ s = s'

Tactic:
have := s.mono_f

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
s s' : S.Splitting
h : s.s = s'.s
this : Mono S.f
⊢ s = s'

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
s s' : S.Splitting
h : s.s = s'.s
this : Mono S.f
⊢ s = s'

Tactic:
have eq := s.id

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
s s' : S.Splitting
h : s.s = s'.s
this : Mono S.f
eq : s.r ≫ S.f + S.g ≫ s.s = 𝟙 S.X₂
⊢ s = s'

Proof state:
case mk.mk
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
this : Mono S.f
r✝ : S.X₂ ⟶ S.X₁
s✝¹ : S.X₃ ⟶ S.X₂
f_r✝¹ : S.f ≫ r✝ = 𝟙 S.X₁
s_g✝¹ : s✝¹ ≫ S.g = 𝟙 S.X₃
id✝¹ : r✝ ≫ S.f + S.g ≫ s✝¹ = 𝟙 S.X₂
s✝ : S.X₃ ⟶ S.X₂
s_g✝ : s✝ ≫ S.g = 𝟙 S.X₃
f_r✝ : S.f ≫ { r := r✝, s := s✝¹, f_r := f_r✝¹, s_g := s_g✝¹, id := id✝¹ }.r = 𝟙 S.X₁
id✝ : { r := r✝, s := s✝¹, f_r := f_r✝¹, s_g := s_g✝¹, id := id✝¹ }.r ≫ S.f + S.g ≫ s✝ = 𝟙 S.X₂
h :
  { r := r✝, s := s✝¹, f_r := f_r✝¹, s_g := s_g✝¹, id := id✝¹ }.s =
    { r := { r := r✝, s := s✝¹, f_r := f_r✝¹, s_g := s_g✝¹, id := id✝¹ }.r, s := s✝, f_r := f_r✝, s_g := s_g✝,
        id := id✝ }.s
⊢ { r := r✝, s := s✝¹, f_r := f_r✝¹, s_g := s_g✝¹, id := id✝¹ } =
    { r := { r := r✝, s := s✝¹, f_r := f_r✝¹, s_g := s_g✝¹, id := id✝¹ }.r, s := s✝, f_r := f_r✝, s_g := s_g✝,
      id := id✝ }

Tactic:
obtain rfl := h

Result:
case mk.mk
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
this : Mono S.f
r✝ : S.X₂ ⟶ S.X₁
s✝ : S.X₃ ⟶ S.X₂
f_r✝¹ : S.f ≫ r✝ = 𝟙 S.X₁
s_g✝¹ : s✝ ≫ S.g = 𝟙 S.X₃
id✝¹ : r✝ ≫ S.f + S.g ≫ s✝ = 𝟙 S.X₂
f_r✝ : S.f ≫ { r := r✝, s := s✝, f_r := f_r✝¹, s_g := s_g✝¹, id := id✝¹ }.r = 𝟙 S.X₁
s_g✝ : { r := r✝, s := s✝, f_r := f_r✝¹, s_g := s_g✝¹, id := id✝¹ }.s ≫ S.g = 𝟙 S.X₃
id✝ :
  { r := r✝, s := s✝, f_r := f_r✝¹, s_g := s_g✝¹, id := id✝¹ }.r ≫ S.f +
      S.g ≫ { r := r✝, s := s✝, f_r := f_r✝¹, s_g := s_g✝¹, id := id✝¹ }.s =
    𝟙 S.X₂
⊢ { r := r✝, s := s✝, f_r := f_r✝¹, s_g := s_g✝¹, id := id✝¹ } =
    { r := { r := r✝, s := s✝, f_r := f_r✝¹, s_g := s_g✝¹, id := id✝¹ }.r,
      s := { r := r✝, s := s✝, f_r := f_r✝¹, s_g := s_g✝¹, id := id✝¹ }.s, f_r := f_r✝, s_g := s_g✝, id := id✝ }

Proof state:
case mk.mk
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
this : Mono S.f
r✝¹ : S.X₂ ⟶ S.X₁
s✝¹ : S.X₃ ⟶ S.X₂
f_r✝¹ : S.f ≫ r✝¹ = 𝟙 S.X₁
s_g✝¹ : s✝¹ ≫ S.g = 𝟙 S.X₃
id✝¹ : r✝¹ ≫ S.f + S.g ≫ s✝¹ = 𝟙 S.X₂
r✝ : S.X₂ ⟶ S.X₁
s✝ : S.X₃ ⟶ S.X₂
f_r✝ : S.f ≫ r✝ = 𝟙 S.X₁
s_g✝ : s✝ ≫ S.g = 𝟙 S.X₃
id✝ : r✝ ≫ S.f + S.g ≫ s✝ = 𝟙 S.X₂
h :
  { r := r✝¹, s := s✝¹, f_r := f_r✝¹, s_g := s_g✝¹, id := id✝¹ }.s =
    { r := r✝, s := s✝, f_r := f_r✝, s_g := s_g✝, id := id✝ }.s
eq :
  { r := r✝¹, s := s✝¹, f_r := f_r✝¹, s_g := s_g✝¹, id := id✝¹ }.r =
    { r := r✝, s := s✝, f_r := f_r✝, s_g := s_g✝, id := id✝ }.r
⊢ { r := r✝¹, s := s✝¹, f_r := f_r✝¹, s_g := s_g✝¹, id := id✝¹ } =
    { r := r✝, s := s✝, f_r := f_r✝, s_g := s_g✝, id := id✝ }

Tactic:
obtain rfl := eq

Result:
case mk.mk
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
this : Mono S.f
r✝ : S.X₂ ⟶ S.X₁
s✝¹ : S.X₃ ⟶ S.X₂
f_r✝¹ : S.f ≫ r✝ = 𝟙 S.X₁
s_g✝¹ : s✝¹ ≫ S.g = 𝟙 S.X₃
id✝¹ : r✝ ≫ S.f + S.g ≫ s✝¹ = 𝟙 S.X₂
s✝ : S.X₃ ⟶ S.X₂
s_g✝ : s✝ ≫ S.g = 𝟙 S.X₃
f_r✝ : S.f ≫ { r := r✝, s := s✝¹, f_r := f_r✝¹, s_g := s_g✝¹, id := id✝¹ }.r = 𝟙 S.X₁
id✝ : { r := r✝, s := s✝¹, f_r := f_r✝¹, s_g := s_g✝¹, id := id✝¹ }.r ≫ S.f + S.g ≫ s✝ = 𝟙 S.X₂
h :
  { r := r✝, s := s✝¹, f_r := f_r✝¹, s_g := s_g✝¹, id := id✝¹ }.s =
    { r := { r := r✝, s := s✝¹, f_r := f_r✝¹, s_g := s_g✝¹, id := id✝¹ }.r, s := s✝, f_r := f_r✝, s_g := s_g✝,
        id := id✝ }.s
⊢ { r := r✝, s := s✝¹, f_r := f_r✝¹, s_g := s_g✝¹, id := id✝¹ } =
    { r := { r := r✝, s := s✝¹, f_r := f_r✝¹, s_g := s_g✝¹, id := id✝¹ }.r, s := s✝, f_r := f_r✝, s_g := s_g✝,
      id := id✝ }

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
s s' : S.Splitting
h : s.s = s'.s
this : Mono S.f
eq : s.r ≫ S.f + S.g ≫ s.s = 𝟙 S.X₂
⊢ s = s'

Tactic:
rw [← s'.id, h, add_left_inj, cancel_mono S.f] at eq

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
s s' : S.Splitting
h : s.s = s'.s
this : Mono S.f
eq : s.r = s'.r
⊢ s = s'

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
s s' : S.Splitting
h : s.s = s'.s
this : Mono S.f
eq : s.r = s'.r
⊢ s = s'

Tactic:
cases s

Result:
case mk
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
s' : S.Splitting
this : Mono S.f
r✝ : S.X₂ ⟶ S.X₁
s✝ : S.X₃ ⟶ S.X₂
f_r✝ : S.f ≫ r✝ = 𝟙 S.X₁
s_g✝ : s✝ ≫ S.g = 𝟙 S.X₃
id✝ : r✝ ≫ S.f + S.g ≫ s✝ = 𝟙 S.X₂
h : { r := r✝, s := s✝, f_r := f_r✝, s_g := s_g✝, id := id✝ }.s = s'.s
eq : { r := r✝, s := s✝, f_r := f_r✝, s_g := s_g✝, id := id✝ }.r = s'.r
⊢ { r := r✝, s := s✝, f_r := f_r✝, s_g := s_g✝, id := id✝ } = s'

Proof state:
case mk
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
s' : S.Splitting
this : Mono S.f
r✝ : S.X₂ ⟶ S.X₁
s✝ : S.X₃ ⟶ S.X₂
f_r✝ : S.f ≫ r✝ = 𝟙 S.X₁
s_g✝ : s✝ ≫ S.g = 𝟙 S.X₃
id✝ : r✝ ≫ S.f + S.g ≫ s✝ = 𝟙 S.X₂
h : { r := r✝, s := s✝, f_r := f_r✝, s_g := s_g✝, id := id✝ }.s = s'.s
eq : { r := r✝, s := s✝, f_r := f_r✝, s_g := s_g✝, id := id✝ }.r = s'.r
⊢ { r := r✝, s := s✝, f_r := f_r✝, s_g := s_g✝, id := id✝ } = s'

Tactic:
cases s'

Result:
case mk.mk
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
this : Mono S.f
r✝¹ : S.X₂ ⟶ S.X₁
s✝¹ : S.X₃ ⟶ S.X₂
f_r✝¹ : S.f ≫ r✝¹ = 𝟙 S.X₁
s_g✝¹ : s✝¹ ≫ S.g = 𝟙 S.X₃
id✝¹ : r✝¹ ≫ S.f + S.g ≫ s✝¹ = 𝟙 S.X₂
r✝ : S.X₂ ⟶ S.X₁
s✝ : S.X₃ ⟶ S.X₂
f_r✝ : S.f ≫ r✝ = 𝟙 S.X₁
s_g✝ : s✝ ≫ S.g = 𝟙 S.X₃
id✝ : r✝ ≫ S.f + S.g ≫ s✝ = 𝟙 S.X₂
h :
  { r := r✝¹, s := s✝¹, f_r := f_r✝¹, s_g := s_g✝¹, id := id✝¹ }.s =
    { r := r✝, s := s✝, f_r := f_r✝, s_g := s_g✝, id := id✝ }.s
eq :
  { r := r✝¹, s := s✝¹, f_r := f_r✝¹, s_g := s_g✝¹, id := id✝¹ }.r =
    { r := r✝, s := s✝, f_r := f_r✝, s_g := s_g✝, id := id✝ }.r
⊢ { r := r✝¹, s := s✝¹, f_r := f_r✝¹, s_g := s_g✝¹, id := id✝¹ } =
    { r := r✝, s := s✝, f_r := f_r✝, s_g := s_g✝, id := id✝ }