-- Mathlib/Data/List/Range.lean
theorem ranges_disjoint (l : List ℕ) :
    Pairwise Disjoint (ranges l)

Proof state:
case cons.left.intro.intro.intro.intro
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
s' : List ℕ
left✝¹ : s' ∈ l.ranges
hs : map (fun x => a + x) s' ∈ map (map fun x => a + x) l.ranges
v : ℕ
left✝ : v ∈ s'
hu : a + v ∈ range a
⊢ False

Tactic:
rw [mem_range] at hu

Result:
case cons.left.intro.intro.intro.intro
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
s' : List ℕ
left✝¹ : s' ∈ l.ranges
hs : map (fun x => a + x) s' ∈ map (map fun x => a + x) l.ranges
v : ℕ
left✝ : v ∈ s'
hu : a + v < a
⊢ False

Proof state:
case hf
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
u v : List ℕ
⊢ Function.Injective fun x => a + x

Tactic:
exact fun u v => Nat.add_left_cancel

Result:
no goals

Proof state:
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
⊢ ∀ {a_1 b : List ℕ}, a_1.Disjoint b → (map (fun x => a + x) a_1).Disjoint (map (fun x => a + x) b)

Tactic:
intro u v

Result:
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
u v : List ℕ
⊢ u.Disjoint v → (map (fun x => a + x) u).Disjoint (map (fun x => a + x) v)

Proof state:
case cons.right
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
⊢ Pairwise (fun a_1 b => (map (fun x => a + x) a_1).Disjoint (map (fun x => a + x) b)) l.ranges

Tactic:
apply Pairwise.imp _ hl

Result:
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
⊢ ∀ {a_1 b : List ℕ}, a_1.Disjoint b → (map (fun x => a + x) a_1).Disjoint (map (fun x => a + x) b)

Proof state:
case cons.left.intro.intro.intro.intro
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
s' : List ℕ
left✝¹ : s' ∈ l.ranges
hs : map (fun x => a + x) s' ∈ map (map fun x => a + x) l.ranges
v : ℕ
left✝ : v ∈ s'
hu : a + v < a
⊢ False

Tactic:
omega

Result:
no goals

Proof state:
case cons
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
⊢ (∀ (a' : List ℕ), a' ∈ map (map fun x => a + x) l.ranges → (range a).Disjoint a') ∧
    Pairwise Disjoint (map (map fun x => a + x) l.ranges)

Tactic:
constructor

Result:
case cons.left
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
⊢ ∀ (a' : List ℕ), a' ∈ map (map fun x => a + x) l.ranges → (range a).Disjoint a'

case cons.right
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
⊢ Pairwise Disjoint (map (map fun x => a + x) l.ranges)

Proof state:
case cons.left
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
⊢ ∀ (a' : List ℕ), a' ∈ map (map fun x => a + x) l.ranges → (range a).Disjoint a'

Tactic:
intro s hs

Result:
case cons.left
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
s : List ℕ
hs : s ∈ map (map fun x => a + x) l.ranges
⊢ (range a).Disjoint s

Proof state:
case cons
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
⊢ Pairwise Disjoint (a :: l).ranges

Tactic:
simp only [ranges, pairwise_cons]

Result:
case cons
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
⊢ (∀ (a' : List ℕ), a' ∈ map (map fun x => a + x) l.ranges → (range a).Disjoint a') ∧
    Pairwise Disjoint (map (map fun x => a + x) l.ranges)

Proof state:
case cons.left.intro.intro
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
s' : List ℕ
left✝ : s' ∈ l.ranges
hs : map (fun x => a + x) s' ∈ map (map fun x => a + x) l.ranges
⊢ (range a).Disjoint (map (fun x => a + x) s')

Tactic:
intro u hu

Result:
case cons.left.intro.intro
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
s' : List ℕ
left✝ : s' ∈ l.ranges
hs : map (fun x => a + x) s' ∈ map (map fun x => a + x) l.ranges
u : ℕ
hu : u ∈ range a
⊢ u ∈ map (fun x => a + x) s' → False

Proof state:
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
u v : List ℕ
⊢ u.Disjoint v → (map (fun x => a + x) u).Disjoint (map (fun x => a + x) v)

Tactic:
apply disjoint_map

Result:
case hf
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
u v : List ℕ
⊢ Function.Injective fun x => a + x

Proof state:
case cons.left
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
s : List ℕ
hs : s ∈ map (map fun x => a + x) l.ranges
⊢ (range a).Disjoint s

Tactic:
obtain ⟨s', _, rfl⟩ := mem_map.mp hs

Result:
case cons.left.intro.intro
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
s' : List ℕ
left✝ : s' ∈ l.ranges
hs : map (fun x => a + x) s' ∈ map (map fun x => a + x) l.ranges
⊢ (range a).Disjoint (map (fun x => a + x) s')

Proof state:
case cons.right
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
⊢ Pairwise Disjoint (map (map fun x => a + x) l.ranges)

Tactic:
rw [pairwise_map]

Result:
case cons.right
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
⊢ Pairwise (fun a_1 b => (map (fun x => a + x) a_1).Disjoint (map (fun x => a + x) b)) l.ranges

Proof state:
case nil

⊢ Pairwise Disjoint [].ranges

Tactic:
exact Pairwise.nil

Result:
no goals

Proof state:
case cons.left.intro.intro
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
s' : List ℕ
left✝ : s' ∈ l.ranges
hs : map (fun x => a + x) s' ∈ map (map fun x => a + x) l.ranges
u : ℕ
hu : u ∈ range a
⊢ (∃ a_1, a_1 ∈ s' ∧ a + a_1 = u) → False

Tactic:
rintro ⟨v, _, rfl⟩

Result:
case cons.left.intro.intro.intro.intro
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
s' : List ℕ
left✝¹ : s' ∈ l.ranges
hs : map (fun x => a + x) s' ∈ map (map fun x => a + x) l.ranges
v : ℕ
left✝ : v ∈ s'
hu : a + v ∈ range a
⊢ False

Proof state:
case cons.left.intro.intro
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
s' : List ℕ
left✝ : s' ∈ l.ranges
hs : map (fun x => a + x) s' ∈ map (map fun x => a + x) l.ranges
u : ℕ
hu : u ∈ range a
⊢ u ∈ map (fun x => a + x) s' → False

Tactic:
rw [mem_map]

Result:
case cons.left.intro.intro
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
s' : List ℕ
left✝ : s' ∈ l.ranges
hs : map (fun x => a + x) s' ∈ map (map fun x => a + x) l.ranges
u : ℕ
hu : u ∈ range a
⊢ (∃ a_1, a_1 ∈ s' ∧ a + a_1 = u) → False