is this assumption necessary?

Stream: lean4

[Jared green]

for c3, i am not sure whether i should assume, or if i can prove from hneg, that \forall g \in n, \forall s t \in g, bcompatible s t -> s = t. i think i need it for case 3.

import Init.Data.List
import Init.PropLemmas
import Mathlib.Algebra.BigOperators.Group.List
import Mathlib.Data.List.Dedup
import Mathlib.Data.List.Pairwise
import Mathlib.Data.List.Join
import Mathlib.Data.List.Basic
import Mathlib.Data.List.Defs
import Mathlib.Data.List.Infix
import Mathlib.Data.List.Lattice
import Mathlib.Data.List.Lemmas
import Mathlib.Data.Bool.AllAny
import Mathlib.Data.Bool.Basic
import Mathlib.Logic.Basic
import Batteries.Data.List.Lemmas
import Aesop
open Classical

variable {α : Type}[h : DecidableEq α]
inductive normalizable α (pred : α -> Prop)
  where
  | atom : α -> (normalizable α pred)
  | And : (normalizable α pred) -> (normalizable α pred) -> normalizable α pred
  | Or : (normalizable α pred) -> (normalizable α pred) -> normalizable α pred
  | Not : normalizable α pred -> normalizable α pred
deriving DecidableEq

namespace normalizable

@[reducible]
def toProp (n : normalizable α pred) : Prop :=
  match n with
  | atom a => pred a
  | And a b =>  toProp a ∧ toProp b
  | Or a b => (toProp a) ∨ toProp b
  | Not i => ¬(toProp i)

@[simp]
theorem toProp_not : toProp (Not n₁) ↔ ¬ toProp n₁ := Iff.rfl

@[simp]
theorem toProp_and : toProp (And n₁ n₂) ↔ toProp n₁ ∧ toProp n₂ := Iff.rfl

@[simp]
theorem toProp_or : toProp (Or n₁ n₂) ↔ toProp n₁ ∨ toProp n₂ := Iff.rfl

@[simp]
theorem toProp_atom {a : α} : toProp (atom a : normalizable α pred) ↔ pred a := Iff.rfl

def wToProp (w : Bool × normalizable α pred) : Prop :=
  if w.fst then toProp w.snd else ¬(toProp w.snd)

def sToProp (s : List (Bool × normalizable α pred)) : Prop :=
  s.all (fun x => wToProp x)

def gToProp (g : List (List (Bool × normalizable α pred))) : Prop :=
  g.any (fun x => sToProp x)

def nToProp (n : List (List (List (Bool × normalizable α pred)))) : Prop :=
  n.all (fun x => gToProp x)

def fToProp (n : List (List (List (normalizable α pred)))) : Prop :=
  n.all (fun x => x.any (fun y => y.all (fun z => toProp z)))

theorem s_nodup : ∀ s : List (Bool × normalizable α pred), ((∀ w : Bool × normalizable α pred,∀ x : Bool × normalizable α pred, w ∈ s ∧ x ∈ s ->
  w.snd == x.snd -> w.fst == x.fst) ∧ s.Nodup) <-> (s.map Prod.snd).Nodup :=
  by
  sorry


def bcompatible (s : List (Bool × normalizable α pred)) (t : List (Bool × normalizable α pred)) : Bool :=
  s.all (fun x => t.all (fun y =>  x.snd == y.snd -> x.fst == y.fst))

theorem all_length_list (c : List a -> Prop): (∀ l : List a, c l) <-> (∀ n : Nat,∀ l:List a , l.length = n -> c l) :=
  by
  sorry

theorem nodup_filter : ∀ (l : List α)(p : α -> Bool),l.Nodup -> (l.filter p).Nodup :=
  by
  sorry

theorem c3 : ∀ n : List (List (List (Bool × normalizable α pred))),
             (coherent n ->
            ¬ (∃ g: List (List (Bool × normalizable α pred)), g ∈ n ∧
            ∃ s : List (Bool × normalizable α pred), s ∈ g ∧
            ∃ h : List (List (Bool × normalizable α pred)),h ∈ n ∧
            ((∃ w : Bool × normalizable α pred , w ∉ s ∧
            ∀ t ∈ h, bcompatible s t -> w ∈ t) ∨ ¬(∃ t ∈ h, bcompatible s t ))) ->
            (∀ g ∈ n, ∀ s ∈ g, ∃ t, List.Subset s t ∧ (t.map Prod.snd).Nodup ∧ (sToProp t -> nToProp n))) :=
  by
  --do induction over the length of n three times
  rw [ all_length_list (fun n => (coherent n ->
            ¬ (∃ g: List (List (Bool × normalizable α pred)), g ∈ n ∧
            ∃ s : List (Bool × normalizable α pred), s ∈ g ∧
            ∃ h : List (List (Bool × normalizable α pred)),h ∈ n ∧
            ((∃ w : Bool × normalizable α pred , w ∉ s ∧
            ∀ t ∈ h, bcompatible s t -> w ∈ t) ∨ ¬(∃ t ∈ h, bcompatible s t ))) ->
            (∀ g ∈ n, ∀ s ∈ g, ∃ t, List.Subset s t ∧ (t.map Prod.snd).Nodup ∧ (sToProp t -> nToProp n))) ) ]
  intro m
  induction' m with m ih
  sorry
  clear ih
  induction' m with m' ih
  sorry
  clear ih
  induction' m' with m'' ih
  sorry
  clear ih
  intro n hn
  induction' m'' with m''' ih
  cases' n with g1 n1
  contradiction
  cases' n1 with g2 n2
  simp at hn
  cases' n2 with g3 n3
  simp at hn
  simp [List.length] at hn
  rw [hn]
  intro hcoh hneg g hg s hs
  simp at hg
  push_neg at hneg
  cases' hg with hg1 hg
  unfold coherent at hcoh
  have hcohs := hcoh g (by rw [hg1];simp) s hs
  rw [← s_nodup] at hcohs
  simp only [beq_iff_eq, and_imp,  implies_true, Bool.false_eq_true,
    imp_false, true_and, Bool.true_eq_false, and_true] at hcohs
  rw [hg1] at hs
  let cross12 := g1.bind (fun s1 => (g2.filter (fun s2 => bcompatible s1 s2)).map (fun s2 => s1 ++ s2.filter (fun x => x ∉ s1)))
  have hcross12 : cross12 = g1.bind (fun s1 => (g2.filter (fun s2 => bcompatible s1 s2)).map (fun s2 => s1 ++ s2.filter (fun x => x ∉ s1))) := by {
    dsimp
  }
  let cross13 := g1.bind (fun s1 => (g3.filter (fun s2 => bcompatible s1 s2)).map (fun s2 => s1 ++ s2.filter (fun x => x ∉ s1)))
  have hcross13 : cross13 = g1.bind (fun s1 => (g3.filter (fun s2 => bcompatible s1 s2)).map (fun s2 => s1 ++ s2.filter (fun x => x ∉ s1))) := by {
    dsimp
  }
  have h_cross12 : ∃ t2 ∈ cross12, s.Subset t2 := by {
    sorry
  }
  have hcompat : ∀ t2 ∈ cross12 ,∃ t3 ∈ cross13, bcompatible t2 t3 := by {
    intro t2 ht2
    by_contra hh
    push_neg at hh
    obtain ⟨ s1,hs1,ht2'⟩ := List.mem_bind.mp ht2
    obtain ⟨ t2', ht2',ht2eq⟩ := List.mem_map.mp ht2'
   --here
    sorry
  }
  sorry
  sorry
  sorry

[Kim Morrison]

You may need to put some extra effort into minimizing this question! :-)

[Jared green]

i have an answer, involving an even stronger assumption i know will work, but i still conjecture i dont need either one.
the basic problem looks like this:

variable (a : Type)

theorem s_nodup : ∀ s : List (Bool × a), ((∀ w : Bool × a,∀ x : Bool × a, w ∈ s ∧ x ∈ s ->
  w.2 = x.2 -> w.fst = x.fst) ∧ s.Nodup) <-> (s.map Prod.snd).Nodup :=
  by
  sorry

theorem thetheorem : ∀ g1 g2 g3 : List (List (Bool × a)), (∀ s : List (Bool × a), (s ∈ g1 ∨ s ∈ g2 ∨ s ∈ g3) -> (s.map (Prod.snd)).Nodup ) -> ∀ s ∈ g1,∀ t ∈ g2, (∀ w1 ∈ s, ∀ w2 ∈ t , w1.2 = w2.2 -> w1.1 = w2.1) -> (∃ t3 ∈ g3,  (∀ w1 ∈ s, ∀ w2 ∈ t3 , w1.2 = w2.2 -> w1.1 = w2.1) ∧ (∀ w1 ∈ t, ∀ w2 ∈ t3 , w1.2 = w2.2 -> w1.1 = w2.1) ) ∨ (∃ w, w ∉ s ∧ w ∉ t ∧ ∀t4 ∈ g3, (∀ w1, w1 ∈ s ∨ w1 ∈ t -> ∀ w2 ∈ t4 , w1.2 = w2.2 -> w1.1 = w2.1) -> w ∈ t4) :=
  by

  sorry