-- Mathlib/Data/Set/Prod.lean
theorem offDiag_union (h : Disjoint s t) :
    (s ∪ t).offDiag = s.offDiag ∪ t.offDiag ∪ s ×ˢ t ∪ t ×ˢ s

Proof state:
case h.mpr.inr.intro
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
h0 : x.1 ∈ t
h1 : x.2 ∈ s
h3 : x.1 = x.2
⊢ False

Tactic:
rw [h3] at h0

Result:
case h.mpr.inr.intro
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
h0 : x.2 ∈ t
h1 : x.2 ∈ s
h3 : x.1 = x.2
⊢ False

Proof state:
case h.mpr.inr.intro
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
h0 : x.2 ∈ t
h1 : x.2 ∈ s
h3 : x.1 = x.2
⊢ False

Tactic:
exact (Set.disjoint_right.mp h h0 h1).elim

Result:
no goals

Proof state:
case h
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
⊢ (x.1 ∈ s ∨ x.1 ∈ t) ∧ (x.2 ∈ s ∨ x.2 ∈ t) ∧ ¬x.1 = x.2 ↔
    ((x.1 ∈ s ∧ x.2 ∈ s ∧ ¬x.1 = x.2 ∨ x.1 ∈ t ∧ x.2 ∈ t ∧ ¬x.1 = x.2) ∨ x.1 ∈ s ∧ x.2 ∈ t) ∨ x.1 ∈ t ∧ x.2 ∈ s

Tactic:
constructor

Result:
case h.mp
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
⊢ (x.1 ∈ s ∨ x.1 ∈ t) ∧ (x.2 ∈ s ∨ x.2 ∈ t) ∧ ¬x.1 = x.2 →
    ((x.1 ∈ s ∧ x.2 ∈ s ∧ ¬x.1 = x.2 ∨ x.1 ∈ t ∧ x.2 ∈ t ∧ ¬x.1 = x.2) ∨ x.1 ∈ s ∧ x.2 ∈ t) ∨ x.1 ∈ t ∧ x.2 ∈ s

case h.mpr
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
⊢ ((x.1 ∈ s ∧ x.2 ∈ s ∧ ¬x.1 = x.2 ∨ x.1 ∈ t ∧ x.2 ∈ t ∧ ¬x.1 = x.2) ∨ x.1 ∈ s ∧ x.2 ∈ t) ∨ x.1 ∈ t ∧ x.2 ∈ s →
    (x.1 ∈ s ∨ x.1 ∈ t) ∧ (x.2 ∈ s ∨ x.2 ∈ t) ∧ ¬x.1 = x.2

Proof state:
α : Type u_1
s t : Set α
h : Disjoint s t
⊢ (s ∪ t).offDiag = s.offDiag ∪ t.offDiag ∪ s ×ˢ t ∪ t ×ˢ s

Tactic:
ext x

Result:
case h
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
⊢ x ∈ (s ∪ t).offDiag ↔ x ∈ s.offDiag ∪ t.offDiag ∪ s ×ˢ t ∪ t ×ˢ s

Proof state:
case h.mpr
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
⊢ ((x.1 ∈ s ∧ x.2 ∈ s ∧ ¬x.1 = x.2 ∨ x.1 ∈ t ∧ x.2 ∈ t ∧ ¬x.1 = x.2) ∨ x.1 ∈ s ∧ x.2 ∈ t) ∨ x.1 ∈ t ∧ x.2 ∈ s →
    (x.1 ∈ s ∨ x.1 ∈ t) ∧ (x.2 ∈ s ∨ x.2 ∈ t) ∧ ¬x.1 = x.2

Tactic:
rintro (((⟨h0, h1, h2⟩|⟨h0, h1, h2⟩)|⟨h0, h1⟩)|⟨h0, h1⟩) <;> simp [*]

Result:
case h.mpr.inl.inr.intro
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
h0 : x.1 ∈ s
h1 : x.2 ∈ t
⊢ ¬x.1 = x.2

case h.mpr.inr.intro
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
h0 : x.1 ∈ t
h1 : x.2 ∈ s
⊢ ¬x.1 = x.2

Proof state:
case h.mp
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
⊢ (x.1 ∈ s ∨ x.1 ∈ t) ∧ (x.2 ∈ s ∨ x.2 ∈ t) ∧ ¬x.1 = x.2 →
    ((x.1 ∈ s ∧ x.2 ∈ s ∧ ¬x.1 = x.2 ∨ x.1 ∈ t ∧ x.2 ∈ t ∧ ¬x.1 = x.2) ∨ x.1 ∈ s ∧ x.2 ∈ t) ∨ x.1 ∈ t ∧ x.2 ∈ s

Tactic:
rintro ⟨h0|h0, h1|h1, h2⟩ <;> simp [h0, h1, h2]

Result:
no goals

Proof state:
case h.mpr.inr.intro
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
h0 : x.1 ∈ t
h1 : x.2 ∈ s
⊢ ¬x.1 = x.2

Tactic:
rintro h3

Result:
case h.mpr.inr.intro
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
h0 : x.1 ∈ t
h1 : x.2 ∈ s
h3 : x.1 = x.2
⊢ False

Proof state:
case h.mpr.inl.inr.intro
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
h0 : x.1 ∈ s
h1 : x.2 ∈ t
h3 : x.1 = x.2
⊢ False

Tactic:
rw [h3] at h0

Result:
case h.mpr.inl.inr.intro
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
h0 : x.2 ∈ s
h1 : x.2 ∈ t
h3 : x.1 = x.2
⊢ False

Proof state:
case h.mpr.inl.inr.intro
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
h0 : x.1 ∈ s
h1 : x.2 ∈ t
⊢ ¬x.1 = x.2

Tactic:
rintro h3

Result:
case h.mpr.inl.inr.intro
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
h0 : x.1 ∈ s
h1 : x.2 ∈ t
h3 : x.1 = x.2
⊢ False

Proof state:
case h
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
⊢ x ∈ (s ∪ t).offDiag ↔ x ∈ s.offDiag ∪ t.offDiag ∪ s ×ˢ t ∪ t ×ˢ s

Tactic:
simp only [mem_offDiag, mem_union, ne_eq, mem_prod]

Result:
case h
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
⊢ (x.1 ∈ s ∨ x.1 ∈ t) ∧ (x.2 ∈ s ∨ x.2 ∈ t) ∧ ¬x.1 = x.2 ↔
    ((x.1 ∈ s ∧ x.2 ∈ s ∧ ¬x.1 = x.2 ∨ x.1 ∈ t ∧ x.2 ∈ t ∧ ¬x.1 = x.2) ∨ x.1 ∈ s ∧ x.2 ∈ t) ∨ x.1 ∈ t ∧ x.2 ∈ s

Proof state:
case h.mpr.inl.inr.intro
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
h0 : x.2 ∈ s
h1 : x.2 ∈ t
h3 : x.1 = x.2
⊢ False

Tactic:
exact Set.disjoint_left.mp h h0 h1

Result:
no goals