-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem containsKey_flatMap_eq_false [BEq α] {γ : Type w} {l : List γ} {f : γ → List ((a : α) × β a)}
    {a : α} (h : ∀ (i : Nat) (h : i < l.length), containsKey a (f l[i]) = false) :
    containsKey a (l.flatMap f) = false

Proof state:
case refine_2
α : Type u
β : α → Type v
inst✝ : BEq α
γ : Type w
f : γ → List ((a : α) × β a)
a : α
g : γ
t : List γ
ih : (∀ (i : Nat) (h : i < t.length), containsKey a (f t[i]) = false) → containsKey a (List.flatMap f t) = false
h : ∀ (i : Nat) (h : i < (g :: t).length), containsKey a (f (g :: t)[i]) = false
i : Nat
hi : i < t.length
⊢ containsKey a (f t[i]) = false

Tactic:
simpa using h (i + 1) (by simp only [List.length_cons]; omega)

Result:
no goals

Proof state:
case refine_1
α : Type u
β : α → Type v
inst✝ : BEq α
γ : Type w
f : γ → List ((a : α) × β a)
a : α
g : γ
t : List γ
ih : (∀ (i : Nat) (h : i < t.length), containsKey a (f t[i]) = false) → containsKey a (List.flatMap f t) = false
h : ∀ (i : Nat) (h : i < (g :: t).length), containsKey a (f (g :: t)[i]) = false
⊢ containsKey a (f g) = false

Tactic:
simpa using h 0 (by simp)

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
γ : Type w
f : γ → List ((a : α) × β a)
a : α
g : γ
t : List γ
ih : (∀ (i : Nat) (h : i < t.length), containsKey a (f t[i]) = false) → containsKey a (List.flatMap f t) = false
h : ∀ (i : Nat) (h : i < (g :: t).length), containsKey a (f (g :: t)[i]) = false
⊢ containsKey a (f g) = false ∧ containsKey a (List.flatMap f t) = false

Tactic:
refine ⟨?_, ?_⟩

Result:
case refine_1
α : Type u
β : α → Type v
inst✝ : BEq α
γ : Type w
f : γ → List ((a : α) × β a)
a : α
g : γ
t : List γ
ih : (∀ (i : Nat) (h : i < t.length), containsKey a (f t[i]) = false) → containsKey a (List.flatMap f t) = false
h : ∀ (i : Nat) (h : i < (g :: t).length), containsKey a (f (g :: t)[i]) = false
⊢ containsKey a (f g) = false

case refine_2
α : Type u
β : α → Type v
inst✝ : BEq α
γ : Type w
f : γ → List ((a : α) × β a)
a : α
g : γ
t : List γ
ih : (∀ (i : Nat) (h : i < t.length), containsKey a (f t[i]) = false) → containsKey a (List.flatMap f t) = false
h : ∀ (i : Nat) (h : i < (g :: t).length), containsKey a (f (g :: t)[i]) = false
⊢ containsKey a (List.flatMap f t) = false

Proof state:
case refine_2
α : Type u
β : α → Type v
inst✝ : BEq α
γ : Type w
f : γ → List ((a : α) × β a)
a : α
g : γ
t : List γ
ih : (∀ (i : Nat) (h : i < t.length), containsKey a (f t[i]) = false) → containsKey a (List.flatMap f t) = false
h : ∀ (i : Nat) (h : i < (g :: t).length), containsKey a (f (g :: t)[i]) = false
⊢ containsKey a (List.flatMap f t) = false

Tactic:
refine ih ?_

Result:
case refine_2
α : Type u
β : α → Type v
inst✝ : BEq α
γ : Type w
f : γ → List ((a : α) × β a)
a : α
g : γ
t : List γ
ih : (∀ (i : Nat) (h : i < t.length), containsKey a (f t[i]) = false) → containsKey a (List.flatMap f t) = false
h : ∀ (i : Nat) (h : i < (g :: t).length), containsKey a (f (g :: t)[i]) = false
⊢ ∀ (i : Nat) (h : i < t.length), containsKey a (f t[i]) = false

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
γ : Type w
f : γ → List ((a : α) × β a)
a : α
g : γ
t : List γ
ih : (∀ (i : Nat) (h : i < t.length), containsKey a (f t[i]) = false) → containsKey a (List.flatMap f t) = false
h : ∀ (i : Nat) (h : i < (g :: t).length), containsKey a (f (g :: t)[i]) = false
i : Nat
hi : i < t.length
⊢ i + 1 < (g :: t).length

Tactic:
simp only [List.length_cons]

Result:
α : Type u
β : α → Type v
inst✝ : BEq α
γ : Type w
f : γ → List ((a : α) × β a)
a : α
g : γ
t : List γ
ih : (∀ (i : Nat) (h : i < t.length), containsKey a (f t[i]) = false) → containsKey a (List.flatMap f t) = false
h : ∀ (i : Nat) (h : i < (g :: t).length), containsKey a (f (g :: t)[i]) = false
i : Nat
hi : i < t.length
⊢ i + 1 < t.length + 1

Proof state:
case refine_2
α : Type u
β : α → Type v
inst✝ : BEq α
γ : Type w
f : γ → List ((a : α) × β a)
a : α
g : γ
t : List γ
ih : (∀ (i : Nat) (h : i < t.length), containsKey a (f t[i]) = false) → containsKey a (List.flatMap f t) = false
h : ∀ (i : Nat) (h : i < (g :: t).length), containsKey a (f (g :: t)[i]) = false
⊢ ∀ (i : Nat) (h : i < t.length), containsKey a (f t[i]) = false

Tactic:
intro i hi

Result:
case refine_2
α : Type u
β : α → Type v
inst✝ : BEq α
γ : Type w
f : γ → List ((a : α) × β a)
a : α
g : γ
t : List γ
ih : (∀ (i : Nat) (h : i < t.length), containsKey a (f t[i]) = false) → containsKey a (List.flatMap f t) = false
h : ∀ (i : Nat) (h : i < (g :: t).length), containsKey a (f (g :: t)[i]) = false
i : Nat
hi : i < t.length
⊢ containsKey a (f t[i]) = false

Proof state:
case nil
α : Type u
β : α → Type v
inst✝ : BEq α
γ : Type w
f : γ → List ((a : α) × β a)
a : α
h : ∀ (i : Nat) (h : i < [].length), containsKey a (f [][i]) = false
⊢ containsKey a (List.flatMap f []) = false

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
γ : Type w
f : γ → List ((a : α) × β a)
a : α
g : γ
t : List γ
ih : (∀ (i : Nat) (h : i < t.length), containsKey a (f t[i]) = false) → containsKey a (List.flatMap f t) = false
h : ∀ (i : Nat) (h : i < (g :: t).length), containsKey a (f (g :: t)[i]) = false
⊢ 0 < (g :: t).length

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
γ : Type w
f : γ → List ((a : α) × β a)
a : α
g : γ
t : List γ
ih : (∀ (i : Nat) (h : i < t.length), containsKey a (f t[i]) = false) → containsKey a (List.flatMap f t) = false
h : ∀ (i : Nat) (h : i < (g :: t).length), containsKey a (f (g :: t)[i]) = false
i : Nat
hi : i < t.length
⊢ i + 1 < t.length + 1

Tactic:
omega

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
γ : Type w
f : γ → List ((a : α) × β a)
a : α
g : γ
t : List γ
ih : (∀ (i : Nat) (h : i < t.length), containsKey a (f t[i]) = false) → containsKey a (List.flatMap f t) = false
h : ∀ (i : Nat) (h : i < (g :: t).length), containsKey a (f (g :: t)[i]) = false
⊢ containsKey a (List.flatMap f (g :: t)) = false

Tactic:
simp only [List.flatMap_cons, containsKey_append, Bool.or_eq_false_iff]

Result:
α : Type u
β : α → Type v
inst✝ : BEq α
γ : Type w
f : γ → List ((a : α) × β a)
a : α
g : γ
t : List γ
ih : (∀ (i : Nat) (h : i < t.length), containsKey a (f t[i]) = false) → containsKey a (List.flatMap f t) = false
h : ∀ (i : Nat) (h : i < (g :: t).length), containsKey a (f (g :: t)[i]) = false
⊢ containsKey a (f g) = false ∧ containsKey a (List.flatMap f t) = false

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
γ : Type w
l : List γ
f : γ → List ((a : α) × β a)
a : α
h : ∀ (i : Nat) (h : i < l.length), containsKey a (f l[i]) = false
⊢ containsKey a (List.flatMap f l) = false

Tactic:
induction l

Result:
case nil
α : Type u
β : α → Type v
inst✝ : BEq α
γ : Type w
f : γ → List ((a : α) × β a)
a : α
h : ∀ (i : Nat) (h : i < [].length), containsKey a (f [][i]) = false
⊢ containsKey a (List.flatMap f []) = false

case cons
α : Type u
β : α → Type v
inst✝ : BEq α
γ : Type w
f : γ → List ((a : α) × β a)
a : α
head✝ : γ
tail✝ : List γ
tail_ih✝ :
  (∀ (i : Nat) (h : i < tail✝.length), containsKey a (f tail✝[i]) = false) →
    containsKey a (List.flatMap f tail✝) = false
h : ∀ (i : Nat) (h : i < (head✝ :: tail✝).length), containsKey a (f (head✝ :: tail✝)[i]) = false
⊢ containsKey a (List.flatMap f (head✝ :: tail✝)) = false