Theorem: Metamath.DJ.ext (Metamath/Translate.lean)

State before:
dj₁ : VR → VR → Prop
irr✝¹ : ∀ {x : VR}, ¬dj₁ x x
symm✝¹ : ∀ {x y : VR}, dj₁ x y → dj₁ y x
dj₂ : VR → VR → Prop
irr✝ : ∀ {x : VR}, ¬dj₂ x x
symm✝ : ∀ {x y : VR}, dj₂ x y → dj₂ y x
h :
  ∀ (a b : VR),
    disj { disj := dj₁, irr := irr✝¹, symm := symm✝¹ } a b ↔ disj { disj := dj₂, irr := irr✝, symm := symm✝ } a b
this : dj₁ = dj₂
⊢ { disj := dj₁, irr := irr✝¹, symm := symm✝¹ } = { disj := dj₂, irr := irr✝, symm := symm✝ }
Tactic:
cases this
State after:
case refl
dj₁ : VR → VR → Prop
irr✝¹ : ∀ {x : VR}, ¬dj₁ x x
symm✝¹ : ∀ {x y : VR}, dj₁ x y → dj₁ y x
irr✝ : ∀ {x : VR}, ¬dj₁ x x
symm✝ : ∀ {x y : VR}, dj₁ x y → dj₁ y x
h :
  ∀ (a b : VR),
    disj { disj := dj₁, irr := irr✝¹, symm := symm✝¹ } a b ↔ disj { disj := dj₁, irr := irr✝, symm := symm✝ } a b
⊢ { disj := dj₁, irr := irr✝¹, symm := symm✝¹ } = { disj := dj₁, irr := irr✝, symm := symm✝ }

State before:
case refl
dj₁ : VR → VR → Prop
irr✝¹ : ∀ {x : VR}, ¬dj₁ x x
symm✝¹ : ∀ {x y : VR}, dj₁ x y → dj₁ y x
irr✝ : ∀ {x : VR}, ¬dj₁ x x
symm✝ : ∀ {x y : VR}, dj₁ x y → dj₁ y x
h :
  ∀ (a b : VR),
    disj { disj := dj₁, irr := irr✝¹, symm := symm✝¹ } a b ↔ disj { disj := dj₁, irr := irr✝, symm := symm✝ } a b
⊢ { disj := dj₁, irr := irr✝¹, symm := symm✝¹ } = { disj := dj₁, irr := irr✝, symm := symm✝ }
Tactic:
rfl
State after:
no goals