case h
α : Type u_1
s t : Set α
x✝ : α × α
a : α
h : Disjoint s t
x : α × α
⊢ x ∈ offDiag (s ∪ t) ↔ x ∈ offDiag s ∪ offDiag t ∪ s ×ˢ t ∪ t ×ˢ s
α : Type u_1
s t : Set α
x : α × α
a : α
h : Disjoint s t
⊢ offDiag (s ∪ t) = offDiag s ∪ offDiag t ∪ s ×ˢ t ∪ t ×ˢ s
ext x
case h
α : Type u_1
s t : Set α
x✝ : α × α
a : α
h : Disjoint s t
x : α × α
⊢ (x.fst ∈ s ∨ x.fst ∈ t) ∧ (x.snd ∈ s ∨ x.snd ∈ t) ∧ ¬x.fst = x.snd ↔
    ((x.fst ∈ s ∧ x.snd ∈ s ∧ ¬x.fst = x.snd ∨ x.fst ∈ t ∧ x.snd ∈ t ∧ ¬x.fst = x.snd) ∨ x.fst ∈ s ∧ x.snd ∈ t) ∨
      x.fst ∈ t ∧ x.snd ∈ s
case h
α : Type u_1
s t : Set α
x✝ : α × α
a : α
h : Disjoint s t
x : α × α
⊢ x ∈ offDiag (s ∪ t) ↔ x ∈ offDiag s ∪ offDiag t ∪ s ×ˢ t ∪ t ×ˢ s
simp only [mem_offDiag, mem_union, ne_eq, mem_prod]
case h.mp
α : Type u_1
s t : Set α
x✝ : α × α
a : α
h : Disjoint s t
x : α × α
⊢ (x.fst ∈ s ∨ x.fst ∈ t) ∧ (x.snd ∈ s ∨ x.snd ∈ t) ∧ ¬x.fst = x.snd →
    ((x.fst ∈ s ∧ x.snd ∈ s ∧ ¬x.fst = x.snd ∨ x.fst ∈ t ∧ x.snd ∈ t ∧ ¬x.fst = x.snd) ∨ x.fst ∈ s ∧ x.snd ∈ t) ∨
      x.fst ∈ t ∧ x.snd ∈ s

case h.mpr
α : Type u_1
s t : Set α
x✝ : α × α
a : α
h : Disjoint s t
x : α × α
⊢ ((x.fst ∈ s ∧ x.snd ∈ s ∧ ¬x.fst = x.snd ∨ x.fst ∈ t ∧ x.snd ∈ t ∧ ¬x.fst = x.snd) ∨ x.fst ∈ s ∧ x.snd ∈ t) ∨
      x.fst ∈ t ∧ x.snd ∈ s →
    (x.fst ∈ s ∨ x.fst ∈ t) ∧ (x.snd ∈ s ∨ x.snd ∈ t) ∧ ¬x.fst = x.snd
case h
α : Type u_1
s t : Set α
x✝ : α × α
a : α
h : Disjoint s t
x : α × α
⊢ (x.fst ∈ s ∨ x.fst ∈ t) ∧ (x.snd ∈ s ∨ x.snd ∈ t) ∧ ¬x.fst = x.snd ↔
    ((x.fst ∈ s ∧ x.snd ∈ s ∧ ¬x.fst = x.snd ∨ x.fst ∈ t ∧ x.snd ∈ t ∧ ¬x.fst = x.snd) ∨ x.fst ∈ s ∧ x.snd ∈ t) ∨
      x.fst ∈ t ∧ x.snd ∈ s
constructor
no goals
case h.mp
α : Type u_1
s t : Set α
x✝ : α × α
a : α
h : Disjoint s t
x : α × α
⊢ (x.fst ∈ s ∨ x.fst ∈ t) ∧ (x.snd ∈ s ∨ x.snd ∈ t) ∧ ¬x.fst = x.snd →
    ((x.fst ∈ s ∧ x.snd ∈ s ∧ ¬x.fst = x.snd ∨ x.fst ∈ t ∧ x.snd ∈ t ∧ ¬x.fst = x.snd) ∨ x.fst ∈ s ∧ x.snd ∈ t) ∨
      x.fst ∈ t ∧ x.snd ∈ s
rintro ⟨h0|h0, h1|h1, h2⟩ <;> simp [h0, h1, h2]
case h.mpr.inl.inr.intro
α : Type u_1
s t : Set α
x✝ : α × α
a : α
h : Disjoint s t
x : α × α
h0 : x.fst ∈ s
h1 : x.snd ∈ t
⊢ ¬x.fst = x.snd

case h.mpr.inr.intro
α : Type u_1
s t : Set α
x✝ : α × α
a : α
h : Disjoint s t
x : α × α
h0 : x.fst ∈ t
h1 : x.snd ∈ s
⊢ ¬x.fst = x.snd
case h.mpr
α : Type u_1
s t : Set α
x✝ : α × α
a : α
h : Disjoint s t
x : α × α
⊢ ((x.fst ∈ s ∧ x.snd ∈ s ∧ ¬x.fst = x.snd ∨ x.fst ∈ t ∧ x.snd ∈ t ∧ ¬x.fst = x.snd) ∨ x.fst ∈ s ∧ x.snd ∈ t) ∨
      x.fst ∈ t ∧ x.snd ∈ s →
    (x.fst ∈ s ∨ x.fst ∈ t) ∧ (x.snd ∈ s ∨ x.snd ∈ t) ∧ ¬x.fst = x.snd
rintro (((⟨h0, h1, h2⟩|⟨h0, h1, h2⟩)|⟨h0, h1⟩)|⟨h0, h1⟩) <;> simp [*]
case h.mpr.inl.inr.intro
α : Type u_1
s t : Set α
x✝ : α × α
a : α
h : Disjoint s t
x : α × α
h0 : x.fst ∈ s
h1 : x.snd ∈ t
h3 : x.fst = x.snd
⊢ False
case h.mpr.inl.inr.intro
α : Type u_1
s t : Set α
x✝ : α × α
a : α
h : Disjoint s t
x : α × α
h0 : x.fst ∈ s
h1 : x.snd ∈ t
⊢ ¬x.fst = x.snd
rintro h3
case h.mpr.inl.inr.intro
α : Type u_1
s t : Set α
x✝ : α × α
a : α
h : Disjoint s t
x : α × α
h0 : x.snd ∈ s
h1 : x.snd ∈ t
h3 : x.fst = x.snd
⊢ False
case h.mpr.inl.inr.intro
α : Type u_1
s t : Set α
x✝ : α × α
a : α
h : Disjoint s t
x : α × α
h0 : x.fst ∈ s
h1 : x.snd ∈ t
h3 : x.fst = x.snd
⊢ False
rw [h3] at h0
no goals
case h.mpr.inl.inr.intro
α : Type u_1
s t : Set α
x✝ : α × α
a : α
h : Disjoint s t
x : α × α
h0 : x.snd ∈ s
h1 : x.snd ∈ t
h3 : x.fst = x.snd
⊢ False
exact (Set.disjoint_left.mp h h0 h1)
case h.mpr.inr.intro
α : Type u_1
s t : Set α
x✝ : α × α
a : α
h : Disjoint s t
x : α × α
h0 : x.fst ∈ t
h1 : x.snd ∈ s
h3 : x.fst = x.snd
⊢ False
case h.mpr.inr.intro
α : Type u_1
s t : Set α
x✝ : α × α
a : α
h : Disjoint s t
x : α × α
h0 : x.fst ∈ t
h1 : x.snd ∈ s
⊢ ¬x.fst = x.snd
rintro h3
case h.mpr.inr.intro
α : Type u_1
s t : Set α
x✝ : α × α
a : α
h : Disjoint s t
x : α × α
h0 : x.snd ∈ t
h1 : x.snd ∈ s
h3 : x.fst = x.snd
⊢ False
case h.mpr.inr.intro
α : Type u_1
s t : Set α
x✝ : α × α
a : α
h : Disjoint s t
x : α × α
h0 : x.fst ∈ t
h1 : x.snd ∈ s
h3 : x.fst = x.snd
⊢ False
rw [h3] at h0
no goals
case h.mpr.inr.intro
α : Type u_1
s t : Set α
x✝ : α × α
a : α
h : Disjoint s t
x : α × α
h0 : x.snd ∈ t
h1 : x.snd ∈ s
h3 : x.fst = x.snd
⊢ False
exact (Set.disjoint_right.mp h h0 h1).elim