diff --git a/src/computability/language.lean b/src/computability/language.lean
index 4830b1a3574bc..6887388863b70 100644
--- a/src/computability/language.lean
+++ b/src/computability/language.lean
@@ -3,10 +3,12 @@ Copyright (c) 2020 Fox Thomson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Fox Thomson
 -/
-import data.finset.basic
+import data.set.lattice
+import data.list.basic
 
 /-!
 # Languages
+
 This file contains the definition and operations on formal languages over an alphabet. Note strings
 are implemented as lists over the alphabet.
 The operations in this file define a [Kleene algebra](https://en.wikipedia.org/wiki/Kleene_algebra)
@@ -15,29 +17,32 @@ over the languages.
 
 universes u v
 
-variables {α : Type u} [dec : decidable_eq α]
+variables {α : Type u}
 
 /-- A language is a set of strings over an alphabet. -/
-@[derive [has_mem (list α), has_singleton (list α), has_insert (list α), complete_lattice]]
+@[derive [has_mem (list α), has_singleton (list α), has_insert (list α), complete_boolean_algebra]]
 def language (α) := set (list α)
 
 namespace language
 
 local attribute [reducible] language
 
+/-- Zero language has no elements. -/
 instance : has_zero (language α) := ⟨(∅ : set _)⟩
+/-- `1 : language α` contains only one element `[]`. -/
 instance : has_one (language α) := ⟨{[]}⟩
 
 instance : inhabited (language α) := ⟨0⟩
 
+/-- The sum of two languages is the union of  -/
 instance : has_add (language α) := ⟨set.union⟩
-instance : has_mul (language α) := ⟨λ l m, (l.prod m).image (λ p, p.1 ++ p.2)⟩
+instance : has_mul (language α) := ⟨set.image2 (++)⟩
 
 lemma zero_def : (0 : language α) = (∅ : set _) := rfl
 lemma one_def : (1 : language α) = {[]} := rfl
 
 lemma add_def (l m : language α) : l + m = l ∪ m := rfl
-lemma mul_def (l m : language α) : l * m = (l.prod m).image (λ p, p.1 ++ p.2) := rfl
+lemma mul_def (l m : language α) : l * m = set.image2 (++) l m := rfl
 
 /-- The star of a language `L` is the set of all strings which can be written by concatenating
   strings from `L`. -/
@@ -54,110 +59,39 @@ lemma mem_mul (l m : language α) (x : list α) : x ∈ l * m ↔ ∃ a b, a ∈
 by simp [mul_def]
 lemma mem_star (l : language α) (x : list α) :
   x ∈ l.star ↔ ∃ S : list (list α), x = S.join ∧ ∀ y ∈ S, y ∈ l :=
-by refl
-
-private lemma mul_assoc_lang (l m n : language α) : (l * m) * n = l * (m * n) :=
-by { ext x, simp [mul_def], tauto {closer := `[subst_vars, simp *] } }
-
-private lemma one_mul_lang (l : language α) : 1 * l = l :=
-by { ext x, simp [mul_def, one_def], tauto {closer := `[subst_vars, simp [*]] } }
-
-private lemma mul_one_lang (l : language α) : l * 1 = l :=
-by { ext x, simp [mul_def, one_def], tauto {closer := `[subst_vars, simp *] } }
-
-private lemma left_distrib_lang (l m n : language α) : l * (m + n) = (l * m) + (l * n) :=
-begin
-  ext x,
-  simp only [mul_def, add_def, exists_and_distrib_left, set.mem_image2, set.image_prod,
-  set.mem_image, set.mem_prod, set.mem_union_eq, set.prod_union, prod.exists],
-  split,
-  { rintro ⟨ y, z, (⟨ hy, hz ⟩ | ⟨ hy, hz ⟩), hx ⟩,
-    { left,
-      exact ⟨ y, hy, z, hz, hx ⟩ },
-    { right,
-      exact ⟨ y, hy, z, hz, hx ⟩ } },
-  { rintro (⟨ y, hy, z, hz, hx ⟩ | ⟨ y, hy, z, hz, hx ⟩);
-    refine ⟨ y, z, _, hx ⟩,
-    { left,
-      exact ⟨ hy, hz ⟩ },
-    { right,
-      exact ⟨ hy, hz ⟩ } }
-end
-
-private lemma right_distrib_lang (l m n : language α) : (l + m) * n = (l * n) + (m * n) :=
-begin
-  ext x,
-  simp only [mul_def, set.mem_image, add_def, set.mem_prod, exists_and_distrib_left, set.mem_image2,
-    set.image_prod, set.mem_union_eq, set.prod_union, prod.exists],
-  split,
-  { rintro ⟨ y, (hy | hy), z, hz, hx ⟩,
-    { left,
-      exact ⟨ y, hy, z, hz, hx ⟩ },
-    { right,
-      exact ⟨ y, hy, z, hz, hx ⟩ } },
-  { rintro (⟨ y, hy, z, hz, hx ⟩ | ⟨ y, hy, z, hz, hx ⟩);
-    refine ⟨ y, _, z, hz, hx ⟩,
-    { left,
-      exact hy },
-    { right,
-      exact hy } }
-end
+iff.rfl
 
 instance : semiring (language α) :=
 { add := (+),
-  add_assoc := by simp [add_def, set.union_assoc],
+  add_assoc := set.union_assoc,
   zero := 0,
-  zero_add := by simp [zero_def, add_def],
-  add_zero := by simp [zero_def, add_def],
-  add_comm := by simp [add_def, set.union_comm],
+  zero_add := set.empty_union,
+  add_zero := set.union_empty,
+  add_comm := set.union_comm,
   mul := (*),
-  mul_assoc := mul_assoc_lang,
+  mul_assoc := λ l m n,
+    by simp only [mul_def, set.image2_image2_left, set.image2_image2_right, list.append_assoc],
   zero_mul := by simp [zero_def, mul_def],
   mul_zero := by simp [zero_def, mul_def],
   one := 1,
-  one_mul := one_mul_lang,
-  mul_one := mul_one_lang,
-  left_distrib := left_distrib_lang,
-  right_distrib := right_distrib_lang }
+  one_mul := λ l, by simp [mul_def, one_def],
+  mul_one := λ l, by simp [mul_def, one_def],
+  left_distrib := λ l m n, by simp only [mul_def, add_def, set.image2_union_right],
+  right_distrib := λ l m n, by simp only [mul_def, add_def, set.image2_union_left] }
 
 @[simp] lemma add_self (l : language α) : l + l = l := sup_idem
 
 lemma star_def_nonempty (l : language α) :
-  l.star = { x | ∃ S : list (list α), x = S.join ∧ ∀ y ∈ S, y ∈ l ∧ y ≠ []} :=
+  l.star = {x | ∃ S : list (list α), x = S.join ∧ ∀ y ∈ S, y ∈ l ∧ y ≠ []} :=
 begin
   ext x,
-  rw star_def,
   split,
-  { rintro ⟨ S, hx, h ⟩,
-    refine ⟨ S.filter (λ l, ¬list.empty l), _, _ ⟩,
-    { rw hx,
-      induction S with y S ih generalizing x,
-      { refl },
-      { rw list.filter,
-        cases y with a y,
-        { apply ih,
-          { intros y hy,
-            apply h,
-            rw list.mem_cons_iff,
-            right,
-            assumption },
-          { refl } },
-        { simp only [true_and, list.join, eq_ff_eq_not_eq_tt, if_true, list.cons_append,
-            list.empty, eq_self_iff_true],
-          rw list.append_right_inj,
-          simp only [eq_ff_eq_not_eq_tt, forall_eq] at ih,
-          apply ih,
-          intros y hy,
-          apply h,
-          rw list.mem_cons_iff,
-          right,
-          assumption } } },
-    { intros y hy,
-      simp only [eq_ff_eq_not_eq_tt, list.mem_filter] at hy,
-      finish } },
-  { rintro ⟨ S, hx, h ⟩,
-    refine ⟨ S, hx, _ ⟩,
-    finish }
+  { rintro ⟨S, rfl, h⟩,
+    refine ⟨S.filter (λ l, ¬list.empty l), by simp, λ y hy, _⟩,
+    rw [list.mem_filter, list.empty_iff_eq_nil] at hy,
+    exact ⟨h y hy.1, hy.2⟩ },
+  { rintro ⟨S, hx, h⟩,
+    exact ⟨S, hx, λ y hy, (h y hy).1⟩ }
 end
 
 lemma le_iff (l m : language α) : l ≤ m ↔ l + m = m := sup_eq_right.symm
@@ -171,21 +105,17 @@ end
 
 lemma le_add_congr {l₁ l₂ m₁ m₂ : language α} : l₁ ≤ m₁ → l₂ ≤ m₂ → l₁ + l₂ ≤ m₁ + m₂ := sup_le_sup
 
+lemma mem_supr {ι : Sort v} {l : ι → language α} {x : list α} :
+  x ∈ (⨆ i, l i) ↔ ∃ i, x ∈ l i :=
+set.mem_Union
+
 lemma supr_mul {ι : Sort v} (l : ι → language α) (m : language α) :
   (⨆ i, l i) * m = ⨆ i, l i * m :=
-begin
-  ext x,
-  simp only [mem_mul, set.mem_Union, exists_and_distrib_left],
-  tauto
-end
+set.image2_Union_left _ _ _
 
 lemma mul_supr {ι : Sort v} (l : ι → language α) (m : language α) :
   m * (⨆ i, l i) = ⨆ i, m * l i :=
-begin
-  ext x,
-  simp only [mem_mul, set.mem_Union, exists_and_distrib_left],
-  tauto
-end
+set.image2_Union_right _ _ _
 
 lemma supr_add {ι : Sort v} [nonempty ι] (l : ι → language α) (m : language α) :
   (⨆ i, l i) + m = ⨆ i, l i + m := supr_sup
@@ -193,56 +123,39 @@ lemma supr_add {ι : Sort v} [nonempty ι] (l : ι → language α) (m : languag
 lemma add_supr {ι : Sort v} [nonempty ι] (l : ι → language α) (m : language α) :
   m + (⨆ i, l i) = ⨆ i, m + l i := sup_supr
 
+lemma mem_pow {l : language α} {x : list α} {n : ℕ} :
+  x ∈ l ^ n ↔ ∃ S : list (list α), x = S.join ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l :=
+begin
+  induction n with n ihn generalizing x,
+  { simp only [mem_one, pow_zero, list.length_eq_zero],
+    split,
+    { rintro rfl, exact ⟨[], rfl, rfl, λ y h, h.elim⟩ },
+    { rintro ⟨_, rfl, rfl, _⟩, refl } },
+  { simp only [pow_succ, mem_mul, ihn],
+    split,
+    { rintro ⟨a, b, ha, ⟨S, rfl, rfl, hS⟩, rfl⟩,
+      exact ⟨a :: S, rfl, rfl, list.forall_mem_cons.2 ⟨ha, hS⟩⟩ },
+    { rintro ⟨_|⟨a, S⟩, rfl, hn, hS⟩; cases hn,
+      rw list.forall_mem_cons at hS,
+      exact ⟨a, _, hS.1, ⟨S, rfl, rfl, hS.2⟩, rfl⟩ } }
+end
+
 lemma star_eq_supr_pow (l : language α) : l.star = ⨆ i : ℕ, l ^ i :=
 begin
   ext x,
-  simp only [star_def, set.mem_Union, set.mem_set_of_eq],
+  simp only [mem_star, mem_supr, mem_pow],
   split,
-  { revert x,
-    rintros _ ⟨ S, rfl, hS ⟩,
-    induction S with x S ih,
-    { use 0,
-      tauto },
-    { specialize ih _,
-      { exact λ y hy, hS _ (list.mem_cons_of_mem _ hy) },
-      { cases ih with i ih,
-        use i.succ,
-        rw [pow_succ, mem_mul],
-        exact ⟨ x, S.join, hS x (list.mem_cons_self _ _), ih, rfl ⟩ } } },
-  { rintro ⟨ i, hx ⟩,
-    induction i with i ih generalizing x,
-    { rw [pow_zero, mem_one] at hx,
-      subst hx,
-      use [[]],
-      tauto },
-    { rw [pow_succ, mem_mul] at hx,
-      rcases hx with ⟨ a, b, ha, hb, hx ⟩,
-      rcases ih b hb with ⟨ S, hb, hS ⟩,
-      use a :: S,
-      rw list.join,
-      refine ⟨hb ▸ hx.symm, λ y, or.rec (λ hy, _) (hS _)⟩,
-      exact hy.symm ▸ ha } }
+  { rintro ⟨S, rfl, hS⟩, exact ⟨_, S, rfl, rfl, hS⟩ },
+  { rintro ⟨_, S, rfl, rfl, hS⟩, exact ⟨S, rfl, hS⟩ }
 end
 
 lemma mul_self_star_comm (l : language α) : l.star * l = l * l.star :=
-by simp [star_eq_supr_pow, mul_supr, supr_mul, ← pow_succ, ← pow_succ']
+by simp only [star_eq_supr_pow, mul_supr, supr_mul, ← pow_succ, ← pow_succ']
 
 @[simp] lemma one_add_self_mul_star_eq_star (l : language α) : 1 + l * l.star = l.star :=
 begin
-  rw [star_eq_supr_pow, mul_supr, add_def, supr_split_single (λ i, l ^ i) 0],
-  have h : (⨆ (i : ℕ), l * l ^ i) = ⨆ (i : ℕ) (h : i ≠ 0), (λ (i : ℕ), l ^ i) i,
-  { ext x,
-    simp only [exists_prop, set.mem_Union, ne.def],
-    split,
-    { rintro ⟨ i, hi ⟩,
-      use [i.succ, nat.succ_ne_zero i],
-      rwa pow_succ },
-    { rintro ⟨ (_ | i), h0, hi ⟩,
-      { contradiction },
-      use i,
-      rwa ←pow_succ } },
-  rw h,
-  refl
+  simp only [star_eq_supr_pow, mul_supr, ← pow_succ, ← pow_zero l],
+  exact sup_supr_nat_succ _
 end
 
 @[simp] lemma one_add_star_mul_self_eq_star (l : language α) : 1 + l.star * l = l.star :=
diff --git a/src/data/list/basic.lean b/src/data/list/basic.lean
index 16f799729f257..9c0723a3d42ba 100644
--- a/src/data/list/basic.lean
+++ b/src/data/list/basic.lean
@@ -2512,13 +2512,23 @@ end
 
 attribute [simp] join
 
-theorem join_eq_nil : ∀ {L : list (list α)}, join L = [] ↔ ∀ l ∈ L, l = []
+@[simp] theorem join_eq_nil : ∀ {L : list (list α)}, join L = [] ↔ ∀ l ∈ L, l = []
 | []     := iff_of_true rfl (forall_mem_nil _)
 | (l::L) := by simp only [join, append_eq_nil, join_eq_nil, forall_mem_cons]
 
 @[simp] theorem join_append (L₁ L₂ : list (list α)) : join (L₁ ++ L₂) = join L₁ ++ join L₂ :=
 by induction L₁; [refl, simp only [*, join, cons_append, append_assoc]]
 
+@[simp] theorem join_filter_empty_eq_ff [decidable_pred (λ l : list α, l.empty = ff)] :
+  ∀ {L : list (list α)}, join (L.filter (λ l, l.empty = ff)) = L.join
+| [] := rfl
+| ([]::L) := by simp [@join_filter_empty_eq_ff L]
+| ((a::l)::L) := by simp [@join_filter_empty_eq_ff L]
+
+@[simp] theorem join_filter_ne_nil [decidable_pred (λ l : list α, l ≠ [])] {L : list (list α)} :
+  join (L.filter (λ l, l ≠ [])) = L.join :=
+by simp [join_filter_empty_eq_ff, ← empty_iff_eq_nil]
+
 lemma join_join (l : list (list (list α))) : l.join.join = (l.map join).join :=
 by { induction l, simp, simp [l_ih] }
 
diff --git a/src/data/set/lattice.lean b/src/data/set/lattice.lean
index dd2302ffeb82e..04ee427082a42 100644
--- a/src/data/set/lattice.lean
+++ b/src/data/set/lattice.lean
@@ -932,19 +932,6 @@ infi_image
 
 end image
 
-section image2
-
-variables (f : α → β → γ) {s : set α} {t : set β}
-
-lemma Union_image_left : (⋃ a ∈ s, f a '' t) = image2 f s t :=
-by { ext y, split; simp only [mem_Union]; rintros ⟨a, ha, x, hx, ax⟩; exact ⟨a, x, ha, hx, ax⟩ }
-
-lemma Union_image_right : (⋃ b ∈ t, (λ a, f a b) '' s) = image2 f s t :=
-by { ext y, split; simp only [mem_Union]; rintros ⟨a, b, c, d, e⟩, exact ⟨c, a, d, b, e⟩,
-     exact ⟨b, d, a, c, e⟩ }
-
-end image2
-
 section preimage
 
 theorem monotone_preimage {f : α → β} : monotone (preimage f) := assume a b h, preimage_mono h
@@ -1020,6 +1007,28 @@ end
 
 end prod
 
+
+section image2
+
+variables (f : α → β → γ) {s : set α} {t : set β}
+
+lemma Union_image_left : (⋃ a ∈ s, f a '' t) = image2 f s t :=
+by { ext y, split; simp only [mem_Union]; rintros ⟨a, ha, x, hx, ax⟩; exact ⟨a, x, ha, hx, ax⟩ }
+
+lemma Union_image_right : (⋃ b ∈ t, (λ a, f a b) '' s) = image2 f s t :=
+by { ext y, split; simp only [mem_Union]; rintros ⟨a, b, c, d, e⟩, exact ⟨c, a, d, b, e⟩,
+     exact ⟨b, d, a, c, e⟩ }
+
+lemma image2_Union_left (s : ι → set α) (t : set β) :
+  image2 f (⋃ i, s i) t = ⋃ i, image2 f (s i) t :=
+by simp only [← image_prod, Union_prod_const, image_Union]
+
+lemma image2_Union_right (s : set α) (t : ι → set β) :
+  image2 f s (⋃ i, t i) = ⋃ i, image2 f s (t i) :=
+by simp only [← image_prod, prod_Union, image_Union]
+
+end image2
+
 section seq
 
 /-- Given a set `s` of functions `α → β` and `t : set α`, `seq s t` is the union of `f '' t` over
diff --git a/src/order/complete_lattice.lean b/src/order/complete_lattice.lean
index e14a0a576d07d..13fea9febbd9a 100644
--- a/src/order/complete_lattice.lean
+++ b/src/order/complete_lattice.lean
@@ -1004,6 +1004,18 @@ begin
   { simp_rw [infi_ge_eq_infi_nat_add, ←nat.add_assoc], },
 end
 
+lemma sup_supr_nat_succ (u : ℕ → α) : u 0 ⊔ (⨆ i, u (i + 1)) = ⨆ i, u i :=
+begin
+  refine eq_of_forall_ge_iff (λ c, _),
+  simp only [sup_le_iff, supr_le_iff],
+  refine ⟨λ h, _, λ h, ⟨h _, λ i, h _⟩⟩,
+  rintro (_|i),
+  exacts [h.1, h.2 i]
+end
+
+lemma inf_infi_nat_succ (u : ℕ → α) : u 0 ⊓ (⨅ i, u (i + 1)) = ⨅ i, u i :=
+@sup_supr_nat_succ (order_dual α) _ u
+
 end
 
 section complete_linear_order